The Coq mailing list

[David Monniaux <David.Monniaux AT ens.fr>]

I'm currently playing with Coq and extraction, and I'm having the 
following problems:
* Since the list constructor of standard OCaml (infix ::) is not (yet) 
usable as a prefix ( :: ), I cannot just tell Coq to extract lists to 
OCaml lists. (Future OCaml versions will allow prefix ( :: ), I'm told.)
* OCaml compiles match e with true -> x1 | false -> x2 less efficiently 
than if e then x1 else x2 (bug report filed, but not fixed so far).

Unless I'm greatly mistaken, this can be fixed by a mere syntactic 
transformation using Camlp4. I suppose I'm not the first person to have 
encountered these problems... So has anybody done the necessary Camlp4 
scripts? :-)