The Coq mailing list

[Michael Day <mikeday AT yeslogic.com>]

Hi Adam,

>   Hint Extern 3 =>
>     match goal with
>     | H : ?X ++ ?Y = nil |- _ => 
>       apply app_eq_nil in H; destruct H; subst
>     end : cpdt.

That looks perfect! But sadly it doesn't quite seem to work :)

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.

Best regards,

Michael

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