Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Dot-qualifying


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

Hello,

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.

Either I don't understand how to do it or there is no info about it.
There is whole section in reference manual, but I didn't succeed.

I tried to look at Coq sources for example, but I didn't figure out how it is done.
I guess that dot-notation is established with external option like -R, but don't understand how.

Sincerely,
Kirill Taran



Archive powered by MHonArc 2.6.18.

Top of Page