From e5f210f51f1dc546fed9fcb986648de8f1302f68 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 24 Oct 2014 11:16:41 +0200
Subject: Fix typo in documentation of the [repeat] tactical.

Closes #3761.---
 doc/refman/RefMan-ltac.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 2b658b15c2..ce2cb277cc 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -373,7 +373,7 @@ We have a repeat loop with:
 \end{quote}
 {\tacexpr} is evaluated to $v$. If $v$ denotes a tactic, this tactic
 is applied to each focused goal independently. If the application
-fails, the tactic is applied recursively to all the generated subgoals
+succeeds, the tactic is applied recursively to all the generated subgoals
 until it eventually fails.  The recursion stops in a subgoal when the
 tactic has failed \emph{to make progress}.  The tactic {\tt repeat
   {\tacexpr}} itself never fails.
-- 
cgit v1.2.3