coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Iterating Ltac tactics

From: Matthieu Sozeau <matthieu.sozeau AT gmail.com>
To: Thomas Strathmann <thomas AT pdp7.org>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Iterating Ltac tactics
Date: Mon, 21 Mar 2011 16:08:34 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to:x-mailer; b=TgB6vq/HsvwM76sYt6hoKdsaPYebuLN5Fgb7alTpe3pJP3JfXs6O2YpZjFb/iRIRde V6eoY0/szaRRSBU8s8EQHvF5t6iAupDdRwz6T40/kcdJ/7qadvOUUzRrKVUvnHWJVymf Ao+FaxIVOqGfArlvRKzrvhPfj+6O72pNRuHN4=

Le 21 mars 2011 � 15:07, Thomas Strathmann a �crit :

> Hi,
>
> I have a (probably simple and possibly born from confusion regarding the
> precise meaning of the Coq documentation) question about "iterating" Ltac
> tactics. As far as I understand you can compose tactics so that a number of
> tactics are applied to the sub-goals generated by applying the first tactic
> of this new compound tactic
> (e.g. T1 ; T2), but 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. ...
>
> would do.

Hi,

maybe you mean "after the fact" application of T to every remaining subgoal?
There is a way to apply T to a specific subgoal n using [n:T], but not to
every
subgoal as far as I know.

-- Matthieu

[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, Matthieu Sozeau