The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 15/12/2016 22:27, Ralf Jung wrote:

>> 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 am not sure how you were able to deduce that from Jason's answer, but
no, modules don't get merged.

Best regards,

Guillaume