The Coq mailing list

[maggesi AT math4.unice.fr (Marco.MAGGESI)]

Hello,

I have two questions on modules.

First question: Is it possible to merge module types?  For instance it
would be useful to have an "Include" directive, eg.

  Module Type Preorder_SIG.
  Parameter T:Type; leq:T->T->Prop.
  Axiom reflexivity : (x:T) (leq x x)
  Axiom transitivity : (x,y,z:T) (leq x y)->(leq y z)->(leq x z).
  End Preorder_SIG.
  
  Module Type Equivalence_SIG.
  Include Preorder.
  Axiom symmetry : (x,y:T) (leq x y)->(leq y x).
  End Equivalence_SIG.


Second question: Why bindings that comes from an "Export" directive
are not considered in the module type?  Example:

  Module Type M_A.
  Parameter A:Type.
  End M_A.
  
  Module Type M_AB.
  Parameter A,B:Type.
  End M_AB.
  
  Module Make_AB [M:M_A] <: M_AB.
  Export M.
  Definition B:=A.
  End Make_AB.

  => Error: No such label A

Thanks,
  -- Marco