The Coq mailing list

[Michael Day <mikeday AT yeslogic.com>]

>   Indeed :). Note that in bigger developments it often makes sense to 
> use patterns such as:
>   crush; custom_tactics; crush.
>   or 
>   repeat progress (crush; custom_tactics).
>   to combine crush with some domain specific tactics.

Right, some proofs end up with crush as every second tactic!

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.

Cheers,

Michael

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