The Coq mailing list

["M. Scott Doerrie" <mdoerri AT cs.jhu.edu>]

I have defined a ModuleType functor and a Module functor somewhat as 
follows.

For discussion assume SIG2 is a Module Type.

Module Type SIG (P: SIG2).

Parameter foo : P.t -> Prop.

End SIG.


Module Impl (P:SIG2).

Definition foo (P:t) : Prop :=  (* implementation *).

End Impl


I can't determine how to declare that Impl is of type SIG?  Use of <: 
and : operators produce syntactic error messages.  I'm sure this is a 
simple example, but I am confused by what I thought was straightforward 
to express.

Scott Doerrie