The Coq mailing list

[Thomas Strathmann <thomas AT pdp7.org>]

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.

        Thomas