From 8ba8385acc7e71fccdb72bfa0908e4f64400c633 Mon Sep 17 00:00:00 2001
From: lmamane
Date: Thu, 22 Feb 2007 12:19:52 +0000
Subject: 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
---
 doc/refman/RefMan-ltac.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 41f38046e0..4d790b480c 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}
-- 
cgit v1.2.3