The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Hello,

here is another example of Coq behavior which I do not understand.

I have a file a.v in subdirectory Test/ and a file b.v in the main directory 
which starts with the line

Require Import Test.a.

I try two things:

1. I compile a.v from the main directory with the command:

coqc Test/a

Then when I try to go over the first line of b.v I get the error message 
saying that the file Test/a.vo contains library a and not library Test.a


2. I compile a.v from the main directory with the command:

coqc -R . Test Test/a

Then when I try to go over the first line of b.v I get the error message 
saying that the file Test/a.vo contains library Test.Test.a and not library 
Test.a


This also feels like a bug.

Vladimir.