The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 09/12/2014 12:47 PM, Jonathan wrote:
> 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?

I'm also getting inundated with warnings of the form:

Warning: Invalid character '?' at beginning of identifier "?1158".

-- Jonathan