The Coq mailing list

[Geoff Reedy <geoff AT programmer-monk.net>]

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.