The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Daniel Schepler wrote:
> Say I have a file which uses both the Ensembles and Reals libraries.  Both
> define a version of In: Ensembles.In is set membership, and RList.In is
> membership of a real in an Rlist (a duplication of "list R").  As far as I can
> tell, it seems to be random which version In will refer to.  Is there any way
> I could use a declaration like
>
> Using Ensembles.In.
>
> if Coq decides on using RList.In, to override that choice?  I couldn't find 
> any
> such thing looking through the reference manual (in particular I read through
> section 2.6 "Libraries and qualified names").
>    

The choice isn't random.  It depends on the order in which you import 
the library modules, just like with 'open' in ML.

You might try [Import Ensembles.] to "bring its symbols to the 
foreground."  That has the potential disadvantage of only working for 
whole modules, not individual identifiers.  You always have the option 
of using commands like [Definition In := Ensembles.In.], where the new 
[In] is definitionally equal to the version you reference, though 
particular tactics may not always take advantage of that fact.  
Notations are another approach (overloadable via notation scopes) that 
is guaranteed to be invisible to tactics.