The Coq mailing list

[Andreas Kägi <acepublic AT fastmail.fm>]

Hello everybody,
sorry about two newbie questions on Module Type/Module usage, but I couldn't
find much documentation on their usage. 
I have to define a Module for a Module Type of the following form:

Module Type MT1.
  Parameter A: Set.

  Inductive t : Set := T.

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

Module M1 : MT1.
  Parameter A: Set.

  (* This doesn't work... *)
  (* Definition d := T. *)

  (* Doesn't work without this *)  
  Module Type MT1sub.
    Parameter B: Set.
  End MT1sub.
  
  Module M1sub : MT1sub.
    Parameter B: Set.
  End M1sub.
End M1.

How can I
(1) access an inductive type definition in the Module definition that comes 
from
the corresponding Module Type?
(2) How can I implement a nested Module Type like the above MT1sub without
repeating the nested Module Type in the Module definition?

Are there solutions other then moving Inductive t resp. ModuleType MT1sub to 
the
top-level?

I don't know if nested module types even make sense but unfortunately I have 
to
implement a couple of modules whose module types are built up like that.

Kind regards,
Andreas