The Coq mailing list

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

On 01/12/2014 09:11 AM, Ian Lynagh wrote:
> Can anyone tell me how I can tell coq that a/b.v should have module name
> a.b please?
>    

See Section 16.4 of CPDT <http://adam.chlipala.net/cpdt/>.

(I should also note that there is some ongoing controversy on this very 
mailing list about how this feature _should_ work!)