Document [> … ].

1 files changed, 31 insertions, 25 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 75aa33d7a1..cf2e708146 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -292,54 +292,60 @@ 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 the goals generated by the
 application of $v_1$. Sequence is left-associative.
 
-\subsubsection[Local sequence]{Local sequence\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]}}
+\subsubsection[Local application of tactics]{Local application of tactics\tacindex{[>\ldots$\mid$\ldots$\mid$\ldots]}\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]}\index{Tacticals![> \mid ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}\index{Tacticals!; [ \mid ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}}
 %\tacindex{; [ | ]}
 %\index{; [ | ]@{\tt ;[\ldots$\mid$\ldots$\mid$\ldots]}}
-\index{Tacticals!; [ \mid ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}
 
-A local sequence has the following form:
+Different tactics can be applied to the different goals using the following form:
 \begin{quote}
-{\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |}
-{\tacexpr}$_n$ {\tt ]}
+{\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 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.
+and all have to be tactics. The $v_i$ is applied to the $i$-th goal,
+for $=1,...,n$. It fails if the number of focused goals is not exactly $n$.
 
 \begin{Variants}
-  \item If no tactic is given for the $i$-th generated subgoal, it
-behaves as if the tactic {\tt idtac} were given. For instance, {\tt
-split ; [ | auto ]} is a shortcut for
-{\tt split ; [ idtac | auto ]}.
+  \item If no tactic is given for the $i$-th goal, it behaves as if
+    the tactic {\tt idtac} were given. For instance, {\tt [~> | auto
+    ]} is a shortcut for {\tt [ > idtac | auto ]}.
 
-  \item {\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |}
+  \item {\tt [ >} {\tacexpr}$_1$ {\tt |} $...$ {\tt |}
     {\tacexpr}$_i$ {\tt |} {\tacexpr} {\tt ..} {\tt |}
     {\tacexpr}$_{i+1+j}$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
 
-  In this variant, {\tt expr} is used for each subgoal numbered from
-  $i+1$ to $i+j$ (assuming $n$ is the number of subgoals).
+  In this variant, {\tt expr} is used for each goal numbered from
+  $i+1$ to $i+j$ (assuming $n$ is the number of goals).
 
   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$.
+  goals numbered from $i+1$ to $i+j$.
 
-  \item {\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |}
+  \item {\tt [ >} {\tacexpr}$_1$ {\tt |} $...$ {\tt |}
     {\tacexpr}$_i$ {\tt |} {\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 idtac} is used for the goals numbered from
   $i+1$ to $i+j$.
 
-  \item {\tacexpr}$_0$ {\tt ; [} {\tacexpr} {\tt ..} {\tt ]}
+  \item {\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.
+    each of the goals, rather than globally. In particular, if there
+    are no goal, the tactic is not run at all. A tactic which
+    expects multiple goals, such as {\tt swap}, would act as if a single
+    goal is focused.
+
+  \item {\tacexpr} {\tt ; [ } {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]} 
+
+    This variant of local tactic application is paired with a
+    sequence.  In this variant, $n$ must be the number of goals
+    generated by the application of {\tacexpr} to each of the
+    individual goals independently. All the above variants work in
+    this form too. Formally, {\tacexpr} {\tt ; [} $...$ {\tt ]} is
+    equivalent to
+    \begin{quote}
+    {\tt [ >} {\tacexpr} {\tt ; [ >} $...$ {\tt ]} {\tt ..} {\tt ]}
+    \end{quote}
 
 \end{Variants}