The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Thanks! This makes sense.

V.


On Jan 1, 2014, at 6:23 PM, Guillaume Melquiond 
<guillaume.melquiond AT inria.fr>
 wrote:

> On 02/01/2014 00:14, Vladimir Voevodsky wrote:
> 
>> This also feels like a bug.
> 
> No, both behaviors are fine; they are intended.
> 
> When you execute "coqc what/ever/a", the resulting module is just "a". So 
> if you import "something.a", you get a mismatch.
> 
> When you execute "coqc -R . something what/ever/a", the resulting module is 
> "something.what.ever.a".
> 
> And if you execute "coqc -R what something what/ever/a", the resulting 
> module is "something.ever.a". So, in your case, you want to use "coqc -R 
> Test Test Test/a" so that the resulting module is "Test.a".
> 
> Best regards,
> 
> Guillaume