diff options
Diffstat (limited to 'doc')
| -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 b90e682df..de8c26943 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -474,7 +474,7 @@ $v_2$). Branching is left-associative. The tactic \begin{quote} -{\tt if {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$} +{\tt tryif {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$} \end{quote} is a generalization of the biased-branching tactics above. The expression {\tacexpr}$_1$ is evaluated to $v_1$, which is then applied @@ -482,7 +482,7 @@ to each subgoal independently. For each goal where $v_1$ succeeds at least once, {tacexpr}$_2$ is evaluated to $v_2$ which is then applied collectively to the generated subgoals. The $v_2$ tactic can trigger backtracking points in $v_1$: where $v_1$ succeeds at least once, {\tt - if {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$} is + tryif {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$} is equivalent to $v_1;v_2$. In each of the goals where $v_1$ does not succeed at least once, {\tacexpr}$_3$ is evaluated in $v_3$ which is is then applied to the goal. |