Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Iterating Ltac tactics

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Iterating Ltac tactics


chronological Thread 
  • 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



Archive powered by MhonArc 2.6.16.

Top of Page