The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 09/12/2014 11:43 AM, Jonathan wrote:
> On 09/12/2014 11:38 AM, Jonathan wrote:
> > 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
>
> Oh - my rebuild didn't fully rebuild.  I need to redo it...
>
> -- Jonathan

Well, having names for evars may be useful, but now Set Printing 
Existential Instances does absolutely nothing.

Also, some change is making [typeclasses eauto with core] loop where 
before it found a solution.

Maybe I git pulled to early?

With this evar naming scheme: I see that the refine-born evars are all 
?GoalN for N being the current number of the corresponding evar 
subgoal.  But, shelve_unifiable hides the evar subgoals (so one no 
longer sees the correspondence), and the cycle/swap/revgoal tactics also 
mess with the correspondence.  Frankly, it was better when the evar ID 
and the subgoal ID corresponded.  Might there be a way to name evars and 
their corresponding subgoals manually?  An intro pattern associated with 
refine?

-- Jonathan