1 files changed, 11 insertions, 8 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 391a78b34..e443ce077 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -218,14 +218,14 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
   rslt;;
 
 
-let catch_failerror e =
+let catch_failerror (e, info) =
   if catchable_exception e then Control.check_for_interrupt ()
   else match e with
   | FailError (0,_) ->
       Control.check_for_interrupt ()
   | FailError (lvl,s) ->
-    raise (Exninfo.copy e (FailError (lvl - 1, s)))
-  | e -> raise e
+    iraise (FailError (lvl - 1, s), info)
+  | e -> iraise (e, info)
   (** FIXME: do we need to add a [Errors.push] here? *)
 
 (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
@@ -233,7 +233,8 @@ let tclORELSE0 t1 t2 g =
   try
     t1 g
   with (* Breakpoint *)
-    | e when Errors.noncritical e -> catch_failerror e; t2 g
+    | e when Errors.noncritical e ->
+      let e = Errors.push e in catch_failerror e; t2 g
 
 (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress,
    then applies t2 *)
@@ -245,7 +246,8 @@ let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2
 let tclORELSE_THEN t1 t2then t2else gls =
   match
     try Some(tclPROGRESS t1 gls)
-    with e when Errors.noncritical e -> catch_failerror e; None
+    with e when Errors.noncritical e ->
+      let e = Errors.push e in catch_failerror e; None
   with
     | None -> t2else gls
     | Some sgl ->
@@ -270,16 +272,17 @@ let ite_gen tcal tac_if continue tac_else gl=
       success:=true;result in
   let tac_else0 e gl=
     if !success then
-      raise e
+      iraise e
     else
       try
         tac_else gl
       with
-        e' when Errors.noncritical e' -> raise e in
+        e' when Errors.noncritical e' -> iraise e in
   try
     tcal tac_if0 continue gl
   with (* Breakpoint *)
-  | e when Errors.noncritical e -> catch_failerror e; tac_else0 e gl
+  | e when Errors.noncritical e ->
+    let e = Errors.push e in catch_failerror e; tac_else0 e gl
 
 (* Try the first tactic and, if it succeeds, continue with
    the second one, and if it fails, use the third one *)