The Coq mailing list

[Michel Levy <michel.levy AT imag.fr>]

I would like to represent the type list of PolyList by the same type in 
Ocaml.
The command "Extract Inductive list => bool["[]" "(::)" ]." could not be 
used, because the (::) is not the
ocaml list constructor. Actually, (::) produces in Ocaml a syntax error.
How is it possible to represent cons (in Coq) by :: (in Ocaml) ?
--
Michel Levy

Laboratoire L.S.R., Bureau C214, B.P.72 - 38042 SAINT MARTIN D'HERES CEDEX 
e.mail : Michel.Levy AT imag.fr    tel :(33)476514022
http://www-lsr.imag.fr/users/Michel.Levy