The Coq mailing list

[Claudio Sacerdoti Coen <sacerdot AT cs.unibo.it>]

 Dear Pierre,

> Module F1_2 (M:S1) : S2.

 Wrong, since after the ":" Coq expects the return type.

> Module F1_2 (M:S1) : S2 M.

 Wrong, since module types cannot be applied.
 [ Notice: this limitation could be lifted ]


However, suppose that you already have a functor F1_2 of type S2.
The following works:

Module F1_2' : S2 := F1_2.

(in the CVS version of Coq the following also works:
 Declare Module K : S2.
)

                                        Cheers,
                                        C.S.C.

-- 
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
Doctor in Computer Science, University of Bologna
E-mail: 
sacerdot AT cs.unibo.it
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------