coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] an evar with a split personality, Jonathan, 09/04/2014
- Re: [Coq-Club] an evar with a split personality, Arnaud Spiwack, 09/04/2014
- Re: [Coq-Club] an evar with a split personality, Jonathan, 09/04/2014
- Re: [Coq-Club] an evar with a split personality, Arnaud Spiwack, 09/12/2014
- Re: [Coq-Club] an evar with a split personality, Jonathan, 09/12/2014
- Re: [Coq-Club] an evar with a split personality, Jonathan, 09/12/2014
- Re: [Coq-Club] an evar with a split personality, Jonathan, 09/12/2014
- Re: [Coq-Club] an evar with a split personality, Jonathan, 09/12/2014
- Re: [Coq-Club] an evar with a split personality, Jonathan, 09/12/2014
- Re: [Coq-Club] an evar with a split personality, Jonathan, 09/12/2014
- Re: [Coq-Club] an evar with a split personality, Matthieu Sozeau, 09/12/2014
- Re: [Coq-Club] an evar with a split personality, Jonathan, 09/12/2014
- Re: [Coq-Club] an evar with a split personality, Hugo Herbelin, 09/13/2014
- Re: [Coq-Club] an evar with a split personality, Jonathan, 09/12/2014
- Re: [Coq-Club] an evar with a split personality, Jonathan, 09/12/2014
- Re: [Coq-Club] an evar with a split personality, Jonathan, 09/12/2014
- Re: [Coq-Club] an evar with a split personality, Arnaud Spiwack, 09/12/2014
- Re: [Coq-Club] an evar with a split personality, Jonathan, 09/04/2014
- Re: [Coq-Club] an evar with a split personality, Arnaud Spiwack, 09/04/2014
Archive powered by MHonArc 2.6.18.