The Coq mailing list

[Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>]

Hello Frédéric,

Le 28 mars 09 à 04:08, Frederic Blanqui a écrit :

> Hello. It seems that the declaration of relations or morphisms is  
> not compatible with the section mechanism. When a relation or a  
> morphism is declared inside a section, then it does not seem to be  
> exported or redeclared as a parametric relation or morphism on the  
> section variables  it depends on. Is there any reason for that?  
> Cheers, Frederic.


Compatibility mainly. If you use the typeclasses commands to declare  
them instead, you can prefix with "Global" for the redeclaration to  
happen. E.g, in pseudo-code:

Section foo.
  Variable A : Type.
  Definition my_rel : relation A.

  Global Instance my_rel_equiv : Equivalence my_rel...

  Definition plus : A -> A.
  Global Instance plus_mor : Morphism (my_rel ==> my_rel) plus.
End foo.

-- Matthieu