The Coq mailing list

[Ewen Denney <denney AT irisa.fr>]

We can use Extract Inductive list => list[nil cons] to bind Coq lists to
Caml lists during extraction, but suppose I want to do the same for the
head function? I would like head in Coq to become hd in Caml, but the
problem is that head is defined in Coq as a total function, which
returns Value x or error.

Is there any simple way to make the link between explicit error values
in Coq and true errors (or imcomplete pattern matching) in Caml?

Ewen