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