The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/19/2016 07:10 PM, Eric Mullen wrote:
> Try making sure that d11 and d10 come into scope before ?1179. Likely what
> happened is that ?1179 can't unify with whatever you have on the right
> side, because it has to unify in the context that existed when it was
> created (not the current context).
>
> I believe that what I've said is true for 8.4, and I think it has changed
> in 8.5.

The changes in 8.5 with respect to evar instantiation are probably not 
sufficient to remedy this usage.  In other words, evars in 8.5 still do 
not accommodate instantiations that were not completely in scope at the 
time the evar was created.  I think the primary enhancement in 8.5 is 
when instantiation candidates that were completely in scope when the 
evar was created become different in some way by the time of 
unification, as through for example induction, inversion, renaming of 
hypotheses, etc..  In such cases, 8.5 will attempt to guess how to 
translate between different instances of the same evar in cases where 
the evolution of the instantiation differs between evar instances.  The 
guess it makes is often, but not always, correct.

-- Jonathan