The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT inria.fr>]

> 
> For example, suppose I want to write a program that uses an equality
> on lists of pairs. In Caml, we just use "=", and in Coq we could
> suppose a parameter eq_listpair, but how can these be connected? There
> isn't an identifier in Caml, as there is for eq_string, say, which
> would allow a link, and I'd rather not have to define the (obvious)
> equality by hand in Coq.

Hi,

A possible solution is to axiomatise all your Coq equalities, and then
to map them onto the Caml equality. Example:

Parameter natEq  : (x,y:nat){x=y}+{~x=y}.
Parameter boolEq : (x,y:bool){x=y}+{~x=y}.

Require Extraction.

Extract Constant natEq  => "(=)".
Extract Constant boolEq => "(=)".

Yours,
Eduardo Gimenez.