The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 09/12/2014 08:29 AM, Arnaud Spiwack wrote:
> > Note that the order of hypotheses in the focused goal can't be used to
> > determine what is being substituted for, because of cases like:
> Since this very morning. And thanks to Hugo Herbelin, the substitutions of
> existential variables are systematically printed (in fact, only the part
> which is not the identity). The printed substitution tells you by name what
> is substituted. This should help users figure how they work.

I just did a git pull and rebuild, but am not seeing any change. What 
should I be looking for?

-- Jonathan