diff options
| -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 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. |