The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

No options at all. The files uuu and uu0 were compiled with the command

coqc Generalities/uuu.v

coqc Generalities/uu0.v

from a copy of Foundations/ outside of user-contrib/ and then copied to 
/user-contrib/Foundations/Generalities/

Are you sure you did not leave a copy of uuu.vo around somewhere other than 
in user-contrib/Foundations/Generalities/uuu.vo ?

Also it is important:

a. To have quotes around all file names.

b. To have two layers i.e. Foundations/Generalities/

V.



On Jan 1, 2014, at 5:51 PM, Guillaume Melquiond wrote:

> On 01/01/2014 23:04, Vladimir Voevodsky wrote:
>> I get an error message:
>> 
>> File "./pathnotations.v", line 2, characters 0-21:
>> Error: Cannot find library uuu in loadpath
> 
> I cannot reproduce this bug. The file in the separate directory compiles 
> just fine and transitively imports uuu. Could you tell us which options you 
> have used to compile the three files? Of particular interest are -I and -R.
> 
> Best regards,
> 
> Guillaume