The Coq mailing list

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

The crush tactic seems to use autorewrite hints, but I don't see how to trigger this kind of extern hint in this way.

  I don't think you can -- autorewrite only uses equality-based hints.

In the meantime, I can always bind it to a new Ltac tactic and call that manually, which would still be shorter than typing out the whole line each time :)

  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.

  Best,

  Adam

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