The Coq mailing list

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

Thanks Elie and Stéphane, I have installed the Beta version and it works 
great ...
but it lead me to a new (but similar) modelling problem :
I'd like to extend a Higer-order module type but it seems not possible.
example :
   Module Type A(B_impl : B).
   ...
   End  A.

   Module Type A2(B_impl : B).
      Include Type A.
here coqtop respond "You cannot Include a higher-order Module or Module 
Type."

Is there a way to Include A applied to B_impl ?

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