diff options
| author | Arnaud Spiwack | 2014-10-24 11:16:41 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-10-24 11:16:41 +0200 |
| commit | e5f210f51f1dc546fed9fcb986648de8f1302f68 (patch) | |
| tree | d2f59a9d67242f46c889107eec225f05308f84ee | |
| parent | 6f6eaa858a2a4268b8c6a63a284e9d07941b511f (diff) | |
Fix typo in documentation of the [repeat] tactical.
Closes #3761.
| -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. |