coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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]
- [Coq-Club] Hints and the crush tactic, Michael Day
- Re: [Coq-Club] Hints and the crush tactic,
Adam Koprowski
- Re: [Coq-Club] Hints and the crush tactic,
Michael Day
- Re: [Coq-Club] Hints and the crush tactic, Michael Day
- Re: [Coq-Club] Hints and the crush tactic,
Adam Koprowski
- Re: [Coq-Club] Hints and the crush tactic,
Michael Day
- Re: [Coq-Club] Hints and the crush tactic, Adam Koprowski
- Re: [Coq-Club] Hints and the crush tactic,
Michael Day
- Re: [Coq-Club] Hints and the crush tactic, Adam Koprowski
- Re: [Coq-Club] Hints and the crush tactic, Adam Chlipala
- Re: [Coq-Club] Hints and the crush tactic, Michael Day
- Re: [Coq-Club] Hints and the crush tactic, Adam Chlipala
- Re: [Coq-Club] Hints and the crush tactic, Matthieu Sozeau
- Re: [Coq-Club] Hints and the crush tactic,
Michael Day
- Re: [Coq-Club] Hints and the crush tactic, Adam Koprowski
- Re: [Coq-Club] Hints and the crush tactic,
Michael Day
- Re: [Coq-Club] Hints and the crush tactic,
Michael Day
- Re: [Coq-Club] Hints and the crush tactic,
Adam Koprowski
Archive powered by MhonArc 2.6.16.