The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

> Maybe I git pulled to early?

Maybe...

Giving names to dependent evars and supporting their parsing together
with their instances is, let's say, in beta-test stage to the
exception of the naming heuristics which will require more
experimentation. Note incidentally that today's trunk solves the
Not_found bug in setoid_rewrite.

Giving names to non-dependent evars and possibly providing ways for
the user to provide names her/himself (as you asked) is experimental
work in progress and I doubt it will lose its experimental status even
for 8.5 (in particular the "Goal"-based naming is not supposed to
remain as it is).

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

That's the point, if it happens that always printing the non-identity
part of the instances is not obfuscating too much what is displayed,
this will be kept by default and there will be no need for "Set
Printing Existential Instances" anymore.

Hugo

On Fri, Sep 12, 2014 at 03:18:41PM -0400, Jonathan wrote:
> On 09/12/2014 03:02 PM, Matthieu Sozeau wrote:
> >Hi Jonathan,
> >
> >   If you’re on the bleeding edge, you can expect to get hurt like this :)
> 
> Certainly!  I'm not complaining - things with regards to evars and
> automation are heading in the right direction (so far as I can tell,
> not having a roadmap) in the trunk - just not necessarily
> monotonically.  I don't expect otherwise.
> 
> I also have little choice, as I've based so much already on the
> typeclasses eauto changes in the trunk, among other changes.
> 
> >I think it might be my doing, I made a change I’m not so sure of to
> >typeclasses eauto in the trunk. Please report this on coq-bugs or coq-dev
> >(https://sympa.inria.fr/sympa/info/coqdev) instead of here.
> >
> >Best,
> >— Matthieu
> 
> OK.  I will (attempt to) use Jason's bug-narrowing scripts...
> 
> -- Jonathan