diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2015-01-21 08:41:38 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-01-21 08:41:38 +0100 |
| commit | fb860f9ea8dca5395ca9f2f350a68c1760c84ce4 (patch) | |
| tree | ac2f64fb20f5a19eb4f47f59af0442984c1e8bcd /doc | |
| parent | 35fde66d67a7a4e36f04adc53347bbb87a34356e (diff) | |
Reference manual: fix typo in doc of [tryif/then/else].
Fixes #3939.
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. |