The Coq mailing list

[Emmanuel Polonowski <polonowski AT u-pec.fr>]

Dear Coq-Club readers,

When using the module system in order to instantiate a functor, I get a 
strange error message.


Module Type A.
End A.

Module Type F (a : A).
End F.

Module G (a : A) (fi : F a).
End G.

Module FI_def (a : A).
End FI_def.

Module FI (a : A) : F a := FI_def a.

Module GI (a : A) := G a (FI a).

Error: Application to not path.

Is the definition of this last module correct ?

Thanks for any hint...

Best regards,
Emmanuel

--
---------------------------------------------------------------
Emmanuel Polonowski
Université Paris-Est Créteil - LACL - ESIAG
http://lacl.u-pec.fr/polonowski/
---------------------------------------------------------------