The Coq mailing list

[Guillaume Dufay <Guillaume.Dufay AT sophia.inria.fr>]

Hello,

We start playing with modules and we face the following problem. 
Assuming we have two modules types declaration, whose one is functor type :

Module Type foo.
Parameter a:Set.
End foo.

Module Type bar [f:foo].
Import f.
Parameter b:a.
End bar.


How do I declare a module of type bar?
We tried the following declaration but without success.

Module imp [f:foo] : (bar f).

Any idea?

Best regards.

--
Guillaume