The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

Suppose one has a goal where the consequent contains an evar.  It seems 
that Coq will only allow that evar to be instantiated by hypotheses that 
existed at the "birth" of that evar - the ancestral goal in the proof 
tree where the evar was first introduced. Otherwise, Coq produces an 
error with a message like 'cannot instantiate "?42" because "H" is not 
in its scope'.

With automation based on pattern matching, the automation might not be 
able to identify the need for the hypothesis that properly instantiates 
the evar until a later goal in the proof.  But, at that point, Coq won't 
allow the instantiation.

When proving by hand - one can then undo back to just before the "birth" 
of the evar and introduce the hypothesis there, then roll forward and do 
the instantiation.  But, how can this be handled with proof automation?

-- Jonathan