The Coq mailing list

[anoun AT labri.fr]

Hi,
Is there a way to extend a Coq signature : that is, to keep all the 
declarations
of the first signature and adding some new specification
Ex:
Module Type Relation.
Parameter A:Set.
Parameter lt_A:A->A->Prop.
Paremeter eq_A:A->A->prop.
End Relation.

we now want to define a signature for equivalence relation and another one for
total order .
Is there a way to do that without copying all the declarations above?!

Module Type Eq_Relation.
Parameter A:Set .
...
Parameter lt_A_refl:forall (a:A), lt_A a a .
...
End Eq_Relation.

Thanks a lot in advance
Houda


----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.