The Coq mailing list

[David Nowak <David.Nowak AT lsv.ens-cachan.fr>]

Hello,

In Coq 8.0beta, I first define two module types S1 and S2:

  Module Type S1.
  ...
  End S1.

  Module Type S2.
  ...
  End S2.

Then I define a functor from S1 to S2:

  Module F (M:S1):S2.
  ...
  End F.

Then I define a third signature S3 which contains a module of type S2:

  Module Type S3.
  Declare Module M : S2.
  End S3.

Finally, I want to define a fourth signature S4 which contains two modules M1 
and M2 of respective types S1 and S3.

  Module Type S4.
  Declare Module M1 : S1.
  Declare Module M2 : S3 with Module M:=F(M1).
  End S4.

But the third line of the previous code is not syntactically correct. However I 
think this definition is meaningful. How can I define S4 with the same 
(intuitive) semantics so that it is accepted by Coq?

Thanks,

--
David Nowak
LSV, CNRS UMR 8643 & ENS de Cachan
61, av. du Président Wilson, 94235 Cachan Cedex, France
tél: +33 1 47 40 75 47   fax: +33 1 47 40 75 21
http://www.lsv.ens-cachan.fr/~nowak/