The Coq mailing list

[St�phane Glondu <steph AT glondu.net>]

Le 08/12/2010 18:50, M. Scott Doerrie a écrit :
> Each module has a signature.  Is it possible to bind this signature to a
> Module Type post-hoc? [...]

If you don't give an explicit signature, the "signature" of a module M 
is M itself. You must turn it into a "Module Type", though, if you want 
to use it as a signature. This can be done by using "Include":

Module Type MT.
  Include M.
End MT.

But be aware that this "signature" keeps bodies of definitions (don't 
forget that there can be arbitrary terms in Coq's types). To use it in a 
useful way, there must be some abstract items (e.g. axioms, parameters) 
in M. There is no way AFAIK to make defined items abstract (except by 
giving an explicit signature that forgets them)... and keep in mind that 
the signature might even be not well typed if you forget all definitions.


Cheers,

--
Stéphane