Update the documentation of Ltac's ";" and ";[…]" to reflect the new multi-goal semantics of tactics.

1 files changed, 24 insertions, 14 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 8e588f4e6..67ab4e467 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -278,24 +278,26 @@ A sequence is an expression of the following form:
 \end{quote}
 The expressions {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated
 to $v_1$ and $v_2$ which have to be tactic values. The tactic $v_1$ is
-then applied and $v_2$ is applied to every subgoal generated by the
+then applied and $v_2$ is applied to the goals generated by the
 application of $v_1$. Sequence is left-associative.
 
-\subsubsection[General sequence]{General sequence\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]}}
+\subsubsection[Local sequence]{Local sequence\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]}}
 %\tacindex{; [ | ]}
 %\index{; [ | ]@{\tt ;[\ldots$\mid$\ldots$\mid$\ldots]}}
 \index{Tacticals!; [ \mid ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}
 
-A general sequence has the following form:
+A local sequence has the following form:
 \begin{quote}
 {\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |}
 {\tacexpr}$_n$ {\tt ]}
 \end{quote}
 The expressions {\tacexpr}$_i$ are evaluated to $v_i$, for $i=0,...,n$
-and all have to be tactics. The tactic $v_0$ is applied and $v_i$ is
-applied to the $i$-th generated subgoal by the application of $v_0$,
-for $=1,...,n$. It fails if the application of $v_0$ does not generate
-exactly $n$ subgoals.
+and all have to be tactics. The tactic $v_0$ is applied independently
+to each focused goal, instead of being applied once to all the goals
+together like in the case of the simple sequence. Then $v_i$ is
+applied to the $i$-th generated subgoal by the application of $v_0$ in
+each goal, for $=1,...,n$. It fails if the application of $v_0$ does
+not generate exactly $n$ subgoals in each of the original goals.
 
 \begin{Variants}
   \item If no tactic is given for the $i$-th generated subgoal, it
@@ -304,21 +306,29 @@ split ; [ | auto ]} is a shortcut for
 {\tt split ; [ idtac | auto ]}.
 
   \item {\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |}
-    {\tacexpr}$_i$ {\tt |} {\tt ..} {\tt |} {\tacexpr}$_{i+1+j}$ {\tt |}
-    $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
+    {\tacexpr}$_i$ {\tt |} {\tacexpr} {\tt ..} {\tt |}
+    {\tacexpr}$_{i+1+j}$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
 
-  In this variant, {\tt idtac} is used for the subgoals numbered from
+  In this variant, {\tt expr} is used for each subgoal numbered from
   $i+1$ to $i+j$ (assuming $n$ is the number of subgoals).
 
   Note that {\tt ..} is part of the syntax, while $...$ is the meta-symbol used
   to describe a list of {\tacexpr} of arbitrary length.
+  subgoals numbered from $i+1$ to $i+j$.
 
   \item {\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |}
-    {\tacexpr}$_i$ {\tt |} {\tacexpr} {\tt ..} {\tt |}
-    {\tacexpr}$_{i+1+j}$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
+    {\tacexpr}$_i$ {\tt |} {\tt ..} {\tt |} {\tacexpr}$_{i+1+j}$ {\tt |}
+    $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
 
-  In this variant, {\tacexpr} is used instead of {\tt idtac} for the
-  subgoals numbered from $i+1$ to $i+j$.
+  In this variant, {\tt idtac} is used for the subgoals numbered from
+  $i+1$ to $i+j$.
+
+  \item {\tacexpr}$_0$ {\tt ; [} {\tacexpr} {\tt ..} {\tt ]}
+
+    In this variant, the tactic {\tacexpr} is applied independently to
+    each of the subgoals generated by {\tacexpr}$_0$, instead of being
+    applied once to all the goal together like in the case of the
+    simple sequence.
 
 \end{Variants}