The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

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

No.  Ltac isn't expressive enough to let the user define new notions of 
hint, since you need some imperativity to roll your own such facility.  
The best technique I've found is to parametrize a tactic by another 
tactic that should be called repeatedly to do "forward mode" 
simplifications.  Barring performance concerns, a loop like [repeat 
progress (crush; yourtac)] achieves the same outcome.