The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

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