The Coq mailing list

[Michael Day <mikeday AT yeslogic.com>]

Hi Adam,

> I'm pretty sure [crush] will solve any goal that [auto] can, because 
> [crush] calls [intuition], which calls [auto].  [eauto] is a different 
> story, which, like Adam Koprowski suggested, I leave out because it can 
> increase proof search time dramatically.

Thanks, that makes sense. Having run into a few situations now where 
eauto is too eager and grabs the wrong hypothesis, perhaps it is good to 
have them as separate tactics.

Oh, do you have any suggestion as to how to make crush apply app_eq_nil 
in hypotheses using hints by any chance? :)

Best regards,

Michael

--
Print XML with Prince!
http://www.princexml.com