The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

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