The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Michael Day wrote:
> One thing that's a little bothersome is that crush cannot solve every 
> goal that auto/eauto can solve. It feels silly to say "crush; eauto" 
> and it would be nice if crush could solve a superset of what auto can.

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.