From 1a8def9dc4380b221b5b457f06b12e0a73a3811a Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:41:35 +0000
Subject: 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
---
 tactics/tacticals.ml | 4 ++--
 1 file 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)
 
-- 
cgit v1.2.3