The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

A question about the new fully-evar-backtracking typeclasses eauto proof 
search mechanism:

I have encountered some goals that "typeclasses eauto with core" fails 
trying to solve (at any depth, dfs or bfs), but it succeeds (quite 
quickly) when the order of arguments of certain constructors is 
changed.  I'm guessing this has something to do with evar instantiations 
across the subgoals, which would get their order changed corresponding 
to the constructor arguments order.

Since the new (trunk, built today) mechanism is a work in progress, I 
don't expect it to be fully functional yet.  But, is it supposed to be 
immune to such things as subgoal order of appearance in the proof search 
tree?

-- Jonathan