The Coq mailing list

[Nicolas BERTAUX <nicolas.bertaux AT etu.upmc.fr>]

Hello,

I have the following problem with applications occurring as effective
parameters of functors:

Module Type S.
End S.

Module F (X : S).
End F.

Module M1.
End M1.

Module Type MT (Y : S).
End MT.

Module M2 (X : S) <: MT(F(X)).
  Module M := M1(F(X)).
End M2.

User error: Application to not path

Why cannot I directly pass an application as effective parameter of a functor?
Is this normal?
Is there any workaround?

Nicolas