The Coq mailing list

[Michael Day <mikeday AT yeslogic.com>]

Hi Adam,

>   Note that auto must solve the goal completely or else it will not 
> change the goal in any way. When you apply this tactic directly does it 
> solve the goal completely? Or just "work" giving a new obligation? Can 
> this new obligation be solved by auto?

Right, it isn't sufficient to solve the whole goal, I was just hoping to 
unpack the hypothesis and subst the equalities with crush and then use 
other tactics to make further progress.

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

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 :)

Cheers,

Michael

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