The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-saarland.de>]

Hello

I have a development in progress and I want to exchange some set data
structure by using FSets. Ideally I would want to _Import_ the final
module to make all the lemmas and functions (add, union, ...) available
by their short names.

Module instance but this also makes the names "t" and "eq" available top
level, leading to naming conflicts with the names used for "intros" all
over the place.

Is there any way to Import a Module hiding selected names. Of course on
can manually do this using:

Definition <name> := MyModule.<name> 

for every function and lemma in the FSet interface and not importing the
module, but this does not look like the optimal solution.

Equivalently, is there some way to qualify a name already in the
context, so that it is no longer available by its short name?

-- 
Regards
Christian