coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Overriding default scoping

From: Daniel Schepler <dschepler AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Overriding default scoping
Date: Sun, 6 Feb 2011 10:43:30 -0800
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=from:to:subject:date:user-agent:mime-version:content-type :content-transfer-encoding:message-id; b=PVQsTcB3t/tgW2gXj8ElBhFX7WSFsxg8LKr7PYD/0fg0+OZWNTbYuMAhX/9Nwsrux0 krTYA7OcZ7MRutV3R9y0PoxOfj7ah4XsbXk8npG4Zn6/ssayiUZoALCte26rS9DgaGHI iyGrGB/iIUFJfpmDlWUh30EaUc4+CN8T+bsL4=

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").
--
Daniel Schepler

[Coq-Club] Overriding default scoping, Daniel Schepler
- Re: [Coq-Club] Overriding default scoping, Adam Chlipala