From fb860f9ea8dca5395ca9f2f350a68c1760c84ce4 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 21 Jan 2015 08:41:38 +0100 Subject: Reference manual: fix typo in doc of [tryif/then/else]. Fixes #3939. --- doc/refman/RefMan-ltac.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc') 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. -- cgit v1.2.3