The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

On 13.12.2016 17:33, Jason Gross wrote:
> I would call this a misfeature or a known design issue.  There is a
> similar issue with module functor application.
> 
> If you just want namespacing, try this module structure instead:
> 
> Module Export foo1.
>   Module bar. ... End bar.
> End foo1.
> 
> Module Export foo2.
>   Module bar. ... End bar.
> End foo2.
> 
> ...
> 
> If you also want [Import bar] to do the right thing, you can create
> another module [bar] which [Export]s all of the inner modules [bar].

So when a module Exports multiple modules with the same name, they
somehow get magically merged?  That's scary.

I thought then when I write "X.foo", Coq first finds module "X" and then
looks for symbol "foo" in it.  But with the merging witnessed above, it
seems like it's actually searching for "X.foo" in one go, and there
could be multiple modules X that it is checking here?

Kind regards,
Ralf