Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] an evar with a split personality

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] an evar with a split personality


Chronological Thread 
  • From: Jonathan <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] an evar with a split personality
  • Date: Fri, 12 Sep 2014 15:18:41 -0400

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




Archive powered by MHonArc 2.6.18.

Top of Page