The Coq mailing list

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

Hi,
I use "Include" to do module derivation and I have a problem.
I have  module types A, B and B1.
   B and B1 are functors with a parameter of type A. B1 derives from B.
Then I have two modules test and test1.
   test take two parameters of type A and B, 
   test1 take two parameters of types A and B1.
   test1 derives from test.
here is the code :

Module Type A.
Parameter a :Type.
End A.

Module Type B (a_impl :A).
Axiom b : a_impl.a->a_impl.a.
End B.

Module Type B1 (a_impl :A).
Include Type B a_impl.
Axiom b1 : a_impl.a->a_impl.a->a_impl.a.
End B1.


Module test (a_impl :A) (b_impl :B).
 Import a_impl.
 Module ba := b_impl a_impl.
 Lemma test :a->a.
 Proof.
   apply ba.b.
 Qed.
End test.

Module test1 (a_impl :A) (b1_impl :B1).
 Include (test a_impl b1_impl).
 Print ba.
 Import a_impl.
 Lemma test2 :a->a->a.
 Proof.
   apply ba.b1.
 Qed.
End test1.

Here is the  problem :  I can't access  the axiom ba.b1  in test1. Whan 
I print ba it give me "Module ba  := (b1_impl a_impl)".
Shouldn't it be of type (B1 A)  and have a field b1 ?

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