The Coq mailing list

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

Thanks again, I'll have a look at it.

Le 1 sept. 2011 à 15:58, Adam Chlipala a écrit :

> Emmanuel Polonowski wrote:
>> Thank you for the hint ! It works fine now...
>> 
>> Is there a document providing an introduction or some explanations about 
>> this point or the fundamentals of the module system ?
>> 
> 
> That information is probably present in Section 2.5 of the Coq manual.  For 
> instance, you can see that the non-terminal "module_expression" clearly 
> only allows application to qualified identifiers ("qualid"s).
> 
> The point and fundamentals of Coq's module system are pretty much the same 
> as for ML module systems.  If you're not familiar with those, you might 
> want to read up on one (e.g., OCaml's).

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