diff options
| author |  lmamane <lmamane@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-22 12:19:52 +0000 |
|---|---|---|
| committer | lmamane <lmamane@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-02-22 12:19:52 +0000 |
| commit | 8ba8385acc7e71fccdb72bfa0908e4f64400c633 (patch) | |
| tree | f078c69c852d30ad97e5005dfe7b41c62f1d3bc2 /doc | |
| parent | 09ceaf1bac341c66c5d733f0358fc9b4b3dbad93 (diff) | |
Documentation of tactical "t1 || t2": t2 is executed if t1 fails to
progress, not only if it fails (i.e. gives an error).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9670 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 41f38046e..4d790b480 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -357,7 +357,7 @@ We can easily branch with the following structure: \end{quote} {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and $v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is applied and if -it fails then $v_2$ is applied. Branching is left associating. +it fails to progress then $v_2$ is applied. Branching is left associating. \subsubsection{First tactic to work} \tacindex{first} |