aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tactics/tacticals.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index fe527a811d..299a1e1768 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -482,14 +482,14 @@ module New = struct
tclINDEPENDENT begin
tclIFCATCH t
(fun () -> tclREPEAT0 t)
- (fun _ -> tclUNIT ())
+ (fun e -> catch_failerror e <*> tclUNIT ())
end
let tclREPEAT t =
tclREPEAT0 (tclPROGRESS t)
let rec tclREPEAT_MAIN0 t =
tclIFCATCH t
(fun () -> tclFOCUS 1 1 (tclREPEAT_MAIN0 t))
- (fun _ -> tclUNIT ())
+ (fun e -> catch_failerror e <*> tclUNIT ())
let tclREPEAT_MAIN t =
tclREPEAT_MAIN0 (tclPROGRESS t)