The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

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.

  Well, crush is "just" a tactic (though a useful one), so why not just extending it to include eauto? Note though, that this can, in some cases, badly influence performance (which I'd guess was the reason for not including it in the first place by A. Chlipala). Alternatively you can just pack crush + eauto together in some other tactic and use it in place of crush, whenever you need eauto.

  Best,

  Adam

-- 
Adam Koprowski   [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate    [http://mlstate.com, 15 rue Berlier, 75013 Paris, France]