Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Dot-qualifying

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Dot-qualifying


Chronological Thread 
  • From: Kirill Taran <kirill.t256 AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Dot-qualifying
  • Date: Thu, 24 Jul 2014 14:05:31 +0400

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




Archive powered by MHonArc 2.6.18.

Top of Page