From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 13841BC75 for ; Wed, 16 Feb 2005 15:41:45 +0100 (CET) Received: from [128.93.8.130] (macadam.inria.fr [128.93.8.130]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j1GEfimr032559 for ; Wed, 16 Feb 2005 15:41:44 +0100 Mime-Version: 1.0 (Apple Message framework v619.2) In-Reply-To: <4206976C.1020305@ens.fr> References: <4206976C.1020305@ens.fr> Content-Type: text/plain; charset=US-ASCII; format=flowed Message-Id: <660e7bd2089b2cdeb00e27313b49c4fc@inria.fr> Content-Transfer-Encoding: 7bit From: Damien Doligez Subject: Re: [Caml-list] prefix :: Date: Wed, 16 Feb 2005 15:41:49 +0100 To: caml-list X-Mailer: Apple Mail (2.619.2) X-Miltered: at nez-perce with ID 42135BA8.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; damien:01 damien:01 caml-list:01 monniaux:01 wrote:01 coq:01 coq:01 ocaml's:01 foobar:01 blabla:01 val:01 bool:01 doligez:01 doligez:01 dev:01 X-Spam-Checker-Version: SpamAssassin 3.0.2 (2004-11-16) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.2 X-Spam-Level: On Feb 6, 2005, at 23:17, David Monniaux wrote: > In order to east the export of Coq programs to Caml, I'd like to be > able to tell Coq that "cons" on list is OCaml's :: operator. > Unfortunately, it is syntactically incorrect to write: > match l with > [] -> foobar > | ::(x,y) -> blabla > > This is a little annoying. Is there anything to do about this? You will be able to do this in 3.09: Objective Caml version 3.09+dev16 (2005-02-16) # let x = (::)(1, []);; val x : int list = [1] # match x with (::)(_, _) -> true | [] -> false;; - : bool = true # -- Damien