The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

> <Module Sec : SecI := SecS.
> 
> which extracts to
> 
> >module Sec = SecS
> 
> that is without its type restriction.
> Note that it also extracts SecI this time, so I guess there is a bug
> in the printer which forgets to extract the module type constraint.
> Am I right, or is it intended for reason I don't know?
> 
> If so, I'll submit a bug/feature request on bugzilla.
> 
> Cédric.
> 

Oups, I didn't see that the mli keeps the type annotation of the module.
So, it is okay not to keep it in the ml file (but I find it strange),
and that also mean you need to extract the full library to have it;
just "Extraction <module>" won't show you the type constraints.

Cédric.