diff options
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 4d790b480c..0fbe6f4687 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -268,7 +268,7 @@ A sequence is an expression of the following form: {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and $v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is then applied and $v_2$ is applied to every subgoal generated by the application of -$v_1$. Sequence is left associating. +$v_1$. Sequence is left-associative. \subsubsection{General sequence} \tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]} @@ -357,7 +357,7 @@ We can easily branch with the following structure: \end{quote} {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and $v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is applied and if -it fails to progress then $v_2$ is applied. Branching is left associating. +it fails to progress then $v_2$ is applied. Branching is left-associative. \subsubsection{First tactic to work} \tacindex{first} |