diff options
| author | Maxime Dénès | 2017-11-08 12:59:53 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-08 12:59:53 +0100 |
| commit | e38df89db1b7cd9d201569a39a6a935299317f3e (patch) | |
| tree | 52ec2c5b251c5b7138850015d37b8f1755bb1c1f | |
| parent | 1cdfd1add9e64796f2be92c3088eb0d0443de2d3 (diff) | |
| parent | b75e6f61d2828a1c4da41f919182dda551ea9d47 (diff) | |
Merge PR #6096: Documentation: "tac1 || tac2" means "first [ progress tac1 | tac2 ]"
| -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 574591185c..5fb4585884 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 |