The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

Hi Jonathan,

  If you’re on the bleeding edge, you can expect to get hurt like this :)
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

On 12 sept. 2014, at 20:34, Jonathan 
<jonikelee AT gmail.com>
 wrote:

> 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
>