The Coq mailing list

[Roman Beslik <beroal AT ukr.net>]

$ coqc -R . A/Foo.v
See "coqc --help".
On 20.06.10 16:50, Edsko de Vries wrote:
> Simple question. Suppose I have a file Foo.v in a directory A, and I
> want to load this file using
>
> Require Import A.Foo
>
> in a script B/Bar.v. If I do
>
> coqc A/Foo.v
> coqc B/Bar.v
>
> then I get
>
> File ".../B/Bar.v", line 1, characters 0-21:
> Error: The file .../A/Foo.vo contains library Foo and not library A.Foo

--
Best regards,
  Roman Beslik.