coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Using modules as namespaces

From: Jason Gross <jasongross9 AT gmail.com>
To: Geoff Reedy <geoff AT programmer-monk.net>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Using modules as namespaces
Date: Thu, 10 Oct 2013 14:22:31 -0400

That's exactly what I want. Thanks!

-Jason

On Thursday, October 10, 2013, Geoff Reedy wrote:

On Thu, Oct 10, 2013 at 01:20:17PM -0400, Jason Gross said
> 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 proper way to do this is to have B.v contain

Require A.
Include A.

[Coq-Club] Using modules as namespaces, Jason Gross, 10/10/2013
- Re: [Coq-Club] Using modules as namespaces, Geoff Reedy, 10/10/2013
  - Re: [Coq-Club] Using modules as namespaces, Jason Gross, 10/10/2013