The Coq mailing list

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

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