The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I would like to use [Module]s as namespaces, in particular allowing qualified access to constants.

For example, I would like to be able to define some things in a module [A], and then do something in a module [B] so that anything I can access as [A.foo] can now be accessed as [B.foo].  The following demonstrates what I would like to do, and that it does not work:

$ cat A.v

Axiom x : Type.

$ cat B.v

Require Export A.

$ cat C.v

Require B.

Check B.x.

$ coqc A B

$ coqc C

File "./C.v", line 2, characters 6-9:

Error: The reference B.x was not found in the current environment.

The reason I want to do this is that I need to split apart definitions into various files (both for dependency reasons, and to increase parallelizability of `make`, and because it's nicer not to put everything into a few monolithic files), but I want to be able to refer to [sum] in "Category/Sum.v" as [Category.sum], not [Category.Sum.sum].  (It seems to me that Coq's namespace facilities are crippled if I can do neither this nor have mix-in namespaces, where I define some constants in one place and other constants in another file, and have them both join the same namespace.)

-Jason