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: Adam Koprowski <adam.koprowski AT gmail.com>
  • To: Michael Day <mikeday AT yeslogic.com>
  • Cc: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Hints and the crush tactic
  • Date: Tue, 30 Mar 2010 11:16:29 +0200
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=GUmFuQA8na4KL4zApXRxmhuvEpbeqMj5llXNIJFmNlH35hYi8YWsL28JXqkT21mFgA KXEdANJ77fd+oea40w3+ixaxhP9z1FLNPDH+wUbJwuIhSh9aGyeOvIwQTzvhL/KgG7Ao Q5c9CihoqRBCVvWzLateB/gC0Al747P7rCfD8=

The crush tactic seems to use autorewrite hints, but I don't see how to trigger this kind of extern hint in this way.
  I don't think you can -- autorewrite only uses equality-based hints.

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 :)
  Indeed :). Note that in bigger developments it often makes sense to use patterns such as:
  crush; custom_tactics; crush.
  or 
  repeat progress (crush; custom_tactics).
  to combine crush with some domain specific tactics.

  Best,
  Adam

--
Adam Koprowski   [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate    [http://mlstate.com, 15 rue Berlier, 75013 Paris, France]



Archive powered by MhonArc 2.6.16.

Top of Page