The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

On Sun, Jan 12, 2014 at 09:13:20AM -0500, Adam Chlipala wrote:
> 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/>.

Aha, thanks! If anyone else is interested, that's "Build Processes" near
the end of the "Proving in the Large" chapter in the HTML version.

But in a nutshell,
    -R . ""
is the flag that i needed.

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

OK, I'll keep an eye out, ta.


Thanks
Ian