diff options
Diffstat (limited to 'doc/refman/RefMan-ltac.tex')
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 41f38046e..4d790b480 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -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 then $v_2$ is applied. Branching is left associating. +it fails to progress then $v_2$ is applied. Branching is left associating. \subsubsection{First tactic to work} \tacindex{first} |