The Coq mailing list

[Thomas Strathmann <thomas AT pdp7.org>]

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