The Coq mailing list

[Jean-Christophe Filliatre <filliatr AT lri.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.

The fact  that there is no name  for generic equality in  ocaml is not
problematic. You can link your extracted code with an ocaml ``header''
declaring :

======================================================================
let equality = (=);;
======================================================================

and extract in Coq your decidable equality over pairs to that function.

-- 
Jean-Christophe FILLIATRE
  
mailto:Jean-Christophe.Filliatre AT lri.fr
  http://www.lri.fr/~filliatr