The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

I have been experimenting (in the trunk version) with the "typeclasses 
eauto with core" tactic as a fully-backtracking alternative to eauto.  
However, there are cases where eauto solves a goal but typeclasses eauto 
with core fails.  Some of these cases are quite trivial, such as 
applying a single constructor when the goal inductive type has a 
Constructors hint (which is visible in Print Hint output), where that 
constructor completely solves the goal.

Is it ever supposed to be the case that typeclasses eauto with core 
fails when eauto succeeds at solving a goal, or is that a potential bug 
with typeclasses eauto with core?  If this is expected behavior, is 
there a way to use typeclasses eauto with core, or something similar 
that does full backtracking over evars, so that it is at least as 
powerful as normal eauto?

-- Jonathan