The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

When experimenting with the evars, using a recent trunk version of Coq, 
I noticed the following:

Set Printing Existential Instances. (*Or, if in CoqIde, use 
View->Display existential variable instances*)
Require Setoid.

Goal forall a b:nat, a=b -> exists c:nat, c = c.
intros a b aeqb.
eexists. (*make an evar*)
match goal with |- ?V = ?V => remember V as e eqn:Q end. (*clone the evar*)
rewrite Q at 2. (*make the consequent and Q look really similar*)
rewrite aeqb. (*rewrite works!  And the two evar contexts for the same 
"e" evar no longer match!*)
Fail exact Q. (*?*)
instantiate (1:=a) in Q. (*??*)


I don't know if this is a bug or a feature.  I guess it could be a 
feature, but then it points out something quite unexpected: that a 
single evar can have multiple different contexts, even within the same 
goal.  I was under the impression that all copies of the same evar 
shared the same single context.

If this is a bug - is the bug that "rewrite aeqb" does anything at all, 
or that it only rewrites one of the contexts?

If this is a feature:

Are all instances of an evar separable this way, or just some? Which ones?

What tactics other than rewrite can be used to modify a specific version 
of an evar's context without modifying the others?  How does one target 
the context with a tactic?

-- Jonathan