The repeat tactic now honors failure levels in ltac.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17030 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 2 deletions

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index fe527a811..299a1e176 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)