coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Thomas Strathmann <thomas AT pdp7.org>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Iterating Ltac tactics
- Date: Mon, 21 Mar 2011 15:18:54 +0100
On 3/21/11 15:10 , Adam Chlipala wrote:
Thomas Strathmann wrote:
I've yet to find a way to apply a tactic T again and again to the
current goal exactly like
T. T. T. T. T. ...
Perhaps [repeat T] would do? None of the structured Ltac support
duplicates exactly the semantics of the period operator, as far as I
know, but that's a feature, not a bug. :)
Sadly, it doesn't. I should have mentioned that [repeat T] behaves like [T] in this particular situation. I had this ominous feeling that it might be a feature that what I want to do is not supported (directly).
It's not earth shattering, but it would have been nice to be able to automate just a tad more given that among other reasons I was drawn to Coq because of the automation facilities.
Thomas
- [Coq-Club] Iterating Ltac tactics, Thomas Strathmann
- Re: [Coq-Club] Iterating Ltac tactics,
Adam Chlipala
- Re: [Coq-Club] Iterating Ltac tactics, Thomas Strathmann
- Re: [Coq-Club] Iterating Ltac tactics, Adam Chlipala
- Re: [Coq-Club] Iterating Ltac tactics,
AUGER Cedric
- Re: [Coq-Club] Iterating Ltac tactics, Thomas Strathmann
- Re: [Coq-Club] Iterating Ltac tactics, Brandon Moore
- Re: [Coq-Club] Iterating Ltac tactics, Thomas Strathmann
- Re: [Coq-Club] Iterating Ltac tactics, Matthieu Sozeau
- Re: [Coq-Club] Iterating Ltac tactics,
Adam Chlipala
Archive powered by MhonArc 2.6.16.