Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Hints and the crush tactic

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Hints and the crush tactic


chronological Thread 
  • From: Michael Day <mikeday AT yeslogic.com>
  • To: Adam Koprowski <adam.koprowski AT gmail.com>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Hints and the crush tactic
  • Date: Tue, 30 Mar 2010 12:44:47 +1100

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



Archive powered by MhonArc 2.6.16.

Top of Page