The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

Hi all,

Can anyone tell me how I can tell coq that a/b.v should have module name
a.b please?

i.e. I want something like this to work:



$ cat a/b.v

Axiom T : Set.


$ cat c.v  

Require Import a.b.

Axiom v : T.


$ coqc a/b.v
$ coqc c.v  
File "./c.v", line 2, characters 0-19:
Error: The file /tmp/r/a/b.vo contains library b and not library a.b
$ 


Thanks
Ian