The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Cedric and Pierre,

> In fact, that's were the magic happens: you must compile B.v
> (which is in the physical path "./A/") onto the logical path "A."
> coqc -I A -as A A/B.v
That is solution! Thanks.

I had compiled B when I was writing here, but I did it with plain "coqc A/B.v".
Now everything is clear, thanks.

Sincerely,
Kirill Taran

On Thu, Jul 24, 2014 at 12:28 PM, Pierre-Evariste Dagand <pedagand AT gmail.com> wrote:

> I tried to do simplest project with possibility to access modules via
> dot-notation:
> $ mkdir A
> $ touch A/B.v
> $ echo "Require Import A.B." >> C.v
>
> And I try "coqc -I A C.v", "coqc -I A -as A C.v"
> and "coqc -R A A C.v", but without success.

Have you compiled B first?

In fact, that's were the magic happens: you must compile B.v (which is
in the physical path "./A/") onto the logical path "A." (the jargon is
defined there [http://coq.inria.fr/distrib/current/refman/Reference-Manual016.html#sec568]).
To do so, you can either use :

coqc -I A -as A A/B.v
# Non-recursive import

or

coqc -R A A A/B.v
# Recursive import

Then, you simply compile C.v in the current physical and logical path:

coqc C.v


But it's probably wiser to use coq_makefile to have these things
generated for you.


Cheers,

--
Pierre