Merge PR #6300: Clarify operation of sequences, fixes #6095

1 files changed, 5 insertions, 4 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 5fb458588..7034c5608 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -311,10 +311,11 @@ A sequence is an expression of the following form:
 \begin{quote}
 {\tacexpr}$_1$ {\tt ;} {\tacexpr}$_2$
 \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 the goals generated by the
-application of $v_1$. Sequence is left-associative.
+The expression {\tacexpr}$_1$ is evaluated to $v_1$, which must be
+a tactic value. The tactic $v_1$ is applied to the current goal,
+possibly producing more goals. Then {\tacexpr}$_2$ is evaluated to
+produce $v_2$, which must be a tactic value. The tactic $v_2$ is applied to
+all the goals produced by the prior application. Sequence is associative.
 
 \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{; [ | ]}