Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]",

not "first [ progress tac1 | progress tac2 ]".

And add a missing backslash.

1 files changed, 2 insertions, 2 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 574591185..5fb458588 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -547,7 +547,7 @@ Yet another way of branching without backtracking is the following structure:
 $v_2$ which must be tactic values. The tactic value $v_1$ is applied in each
 subgoal independently and if it fails \emph{to progress} then $v_2$ is
 applied. {\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$ is equivalent to {\tt
-  first [} {\tt progress} {\tacexpr}$_1$ {\tt |} {\tt progress}
+  first [} {\tt progress} {\tacexpr}$_1$ {\tt |}
   {\tacexpr}$_2$ {\tt ]} (except that if it fails, it fails like
 $v_2$). Branching is left-associative.
 
@@ -561,7 +561,7 @@ The tactic
 is a generalization of the biased-branching tactics above. The
 expression {\tacexpr}$_1$ is evaluated to $v_1$, which is then applied
 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
+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
   tryif {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$} is