Our module system strongly uses the notion of names. Any objects (theorems, terms, ...) has a distinct name. Therefore, if you want to merge two modules which both declare an object with the same name, this two objects must coincide after merging.
Here are the conditions under which two objects can coincide:
If one of this condition is not respected, the loading of modules will fail.
These rules allow you to make coincide an axiom with a theorem and a constant with a definition. This is why we can prove axiomatic properties of a structure like groups by adding some constants and axioms and then use this module on a particular group where the axioms may be proven and the constants may already exists.