The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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).