From e5aeb8be39853750e3b1526c29cbc6acb323d037 Mon Sep 17 00:00:00 2001
From: glondu
Date: Thu, 17 Sep 2009 15:57:20 +0000
Subject: Clarify documentation of ltac repeat

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12335 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-ltac.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index d5c8cf4edc..2fc8b48b0b 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -338,10 +338,10 @@ We have a repeat loop with:
 {\tt repeat} {\tacexpr}
 \end{quote}
 {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
-applied until it fails. Supposing $n>1$, after the first application
-of $v$, $v$ is applied, at least once, to the generated subgoals and
+applied until it fails. After the first application
+of $v$, $v$ is applied to the generated subgoals and
 so on. It stops when it fails for all the generated subgoals. It never
-fails.
+fails itself.
 
 \subsubsection[Error catching]{Error catching\tacindex{try}
 \index{Tacticals!try@{\tt try}}}
-- 
cgit v1.2.3