The Coq mailing list

[Ewen Denney <denney AT irisa.fr>]

Hello,

Is there a simple way of linking or importing ML equalities in general?

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.

Ewen