The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

When you write the following line:

Module M1 : MT1.

You promise that you are going to build a module that satisfies
the interface declared in the module type MT1, so you have to
produce a value named A of type Set, you have to produce an
inductive type of name t and type Set with a constructor T,
and you have to produce a submodule type with the same characteristics
as in the module type MT1 (not an instance of the module MT1sub, but
another module type, with the same name and fields).  The following
session works (in coq-8.2beta4):

Module Type MT1.
 Parameter A: Set.

 Inductive t : Set := T.

 Module Type MT1sub.
   Parameter B: Set.
 End MT1sub.
End MT1.

Module M1 : MT1.

 Definition A := nat.

 Inductive t : Set := T.

 Module Type MT1sub.
   Parameter B: Set.
 End MT1sub.
End M1.

Right now, I don't see why you would want to have a module type
inside another module type (like you did with MT1sub), but it is
possible.

I hope this helps,

Yves