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 14:34:14 -0400

On 09/12/2014 02:07 PM, Jonathan wrote:
On 09/12/2014 12:47 PM, Jonathan wrote:

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

Preliminary analysis suggests that some recent change is causing more instances of something like bug #3381, where usage of [typeclasses eauto with core] can cause evars that aren't involved in the targeted subgoal to get instantiated, blocking the solution of other subgoals.

Is it possible that [typeclasses eauto with core] doesn't properly undo instantiations after failing (or giving up due to depth) along certain search paths?

The change is between Sept 9 and today.

-- Jonathan


There are also more cases of something like bug #3417: "Anomaly: Uncaught exception Not_found(_). Please report." when trying to setoid_rewrite under binders.

-- Jonathan




Archive powered by MHonArc 2.6.18.

Top of Page