The Coq mailing list

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

I'm puzzled by the reference in this document to, firstly,
for i = 0, ..., n
and secondly,
for i = 1, ..., n

Is one of these a typo, or what is the relevance of expr0?

And further down that page, it says

Variant expr0 ; [expri*|]

     This variant of local tactic application is paired with a sequence. 
In this variant, there must be as many expri as goals generated by the 
application of expr0 to each of the individual goals independently. All 
the above variants work in this form too. Formally, expr ; [ ... ] is 
equivalent to [> expr ; [> ... ] .. ].

In this passage, what does "each of the individual goals" refer to?
And, what does the three dots refer to?  Is a sort of meta-symbol, 
whereas the two dots is something that is typed in literally?

And, by way of an illustrative example, what is the difference between

tac1 ; [ tac2 | tac3 ]
and
tac1 ; [> tac2 | tac3 ]

Thanks

Jeremy


On 01/24/2019 12:15 AM, Théo Zimmermann wrote:
> See 
> https://coq.inria.fr/refman/proof-engine/ltac.html#coq:tacn.dispatch, 
> for the documentation of [> foo .. ].