The Coq mailing list

[Michael Day <mikeday AT yeslogic.com>]

> Is the name of the hypothesis significant, or will it match any 
> hypothesis with that form? Is the number 3 important? Is the syntax 
> correct? I've tried adding some fail tactics to debug it, but they never 
> seem to trigger.

Following up on this, I can apply this tactic directly in the proof and 
it does work:

match goal with | H : ?X ++ ?Y = nil |- _ => apply app_eq_nil in H end.

So clearly matching the hypothesis isn't the problem. Perhaps the crush 
tactic isn't using the hint? I'm not sure how to check that.

Cheers,

Michael

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