diff options
| author | aspiwack | 2013-11-04 18:08:48 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-04 18:08:48 +0000 |
| commit | 84b30df7b5ef9479a89de322bceee5619405d195 (patch) | |
| tree | d9a4a351e60041fb5a989379cc23e41ad0ca0142 /tactics | |
| parent | 5f4a61935e048a8e4490f5610e551d8844a373c4 (diff) | |
Fix Tacticals.New.tclREPEAT_MAiN: does not fail badly when every goal was solved.
This made "autorewrite using tac" fail.
Spotted in CoLoR and Demos.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17059 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacticals.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index f815830ca2..639c4c97bc 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -495,7 +495,7 @@ module New = struct tclREPEAT0 (tclPROGRESS t) let rec tclREPEAT_MAIN0 t = tclIFCATCH t - (fun () -> tclFOCUS 1 1 (tclREPEAT_MAIN0 t)) + (fun () -> tclTRYFOCUS 1 1 (tclREPEAT_MAIN0 t)) (fun e -> catch_failerror e <*> tclUNIT ()) let tclREPEAT_MAIN t = tclREPEAT_MAIN0 (tclPROGRESS t) |