The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

Oh, and did you try the coq_makefile utility ? (not sure of the name)
Maybe it could help you to understand the compilation mechanism of Coq.

2014-07-24 9:54 GMT+02:00 Kirill Taran <kirill.t256 AT gmail.com>:

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

--
.../Sedrikov\...