The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

OK, so I'm understanding that all:tac is a tactic which does a bit of 
tac on each goal, then a bit more of tac on each goal, and so forth, is 
that correct?

If so then how do I find out or work out what the relevant bits of tac 
are? (eg, if tac is actually repeat tac')

For example, based on what you say I might guess that
all : repeat tac
goes back and forth between two goals, applying tac to each (as though 
one instance of tac counted a bit of (repeat tac) - but it seems that is 
not what happens (eg as in my emails in the thread
Re: [Coq-Club] goal selectors; tactic expressions)

Cheers,

Jeremy

On 01/28/2019 11:53 PM, Pierre Courtieu wrote:
> Le lun. 28 janv. 2019 à 13:48, Jeremy Dawson
> <Jeremy.Dawson AT anu.edu.au>
>   a écrit :
>> Thanks, but the words GLOBALLY and INDEPENDENTLY are the words used in
>> the documentation (which, as I said, I don't understand).  What do they
>> mean?
> Globally means that a tactic must be seen as a function taking n goals
> and returning m goals. Hence "all:tac" is ONE tactic that applies to
> ALL goals at once (even if it does it sequentially).
> 
> P.
>