The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Thomas Strathmann wrote:
> 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.

My idea of an automated proof always contains exactly one period 
operator.  Perhaps if you shared more details of your proof task we 
could suggest a different way of structuring it?