The Coq mailing list

[Julien Tesson <julien.tesson AT univ-orleans.fr>]

Hi,
I have the following modelling problem :
I have two module types which contain some similar fields and I'd like 
to factorize them in one module.

example :
for two module B1 and B2

Module Type B1.
   Parameter C : Set.
   Parameter rel : C->C->Prop.

 Axiom  rel_trans :
   forall (c1 c2 c3 : C) , rel c1 c2-> rel c2 c3 -> rel c1 c3.

   Axiom Specific_B1_Axiom :
             forall (c : C) ...
End B1.

Module Type B2.
   Parameter C : Set.
   Parameter rel : C->C->Prop.

 Axiom  rel_trans :
   forall (c1 c2 c3 : C) , rel c1 c2-> rel c2 c3 -> rel c1 c3.

   Axiom Specific_B2_Axiom :
        forall (c : C) ...
End B2.

 I'd like to do something like

Module Type B.
   Parameter C : Set.
   Parameter rel : C->C->Prop.

 Axiom  rel_trans :
   forall (c1 c2 c3 : C) , rel c1 c2-> rel c2 c3 -> rel c1 c3.
End B.

and deriving from B the module types B1 and B2 that embed their specific 
axioms.

The coq'art suggest to write
Module Type B1.
   Declare Module root : B.
   Axiom Specific_B1_Axiom :
      ...
End B1.

but it's not satisfying to me because it force to use B1.root.C to 
access C instead of B1.C .

Is there a way to derive a module from an other one  more transparently 
so that I can access C through B1.C ?

Best Regards,
Julien.
begin:vcard
fn:Julien Tesson
n:Tesson;Julien
org;quoted-printable:Laboratoire d'Informatique Fondamentale d'Orl=C3=A9ans
email;internet:julien.tesson AT univ-orleans.fr
title:Doctorant
tel;work:+33/(0) 2 38 41 72 68
tel;fax:+33/(0) 9 55 33 36 68
x-mozilla-html:TRUE
url:http://tesson.julien.free.fr/
version:2.1
end:vcard