Move the FailError exception from Refiner to Tacticals.

4 files changed, 22 insertions, 9 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 4156d5f0ee..82ce2234e3 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1183,7 +1183,7 @@ let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique =
       try
         Proofview.V82.of_tactic
         (Search.eauto_tac (modes,st) ~only_classes:true ~depth [hints] ~dep:true) gls
-      with Refiner.FailError _ -> raise Not_found
+      with Tacticals.FailError _ -> raise Not_found
   in
   let evd = sig_sig gls' in
   let t' = mkEvar (ev, subst) in
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index d275e15255..686303a2ab 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -206,7 +206,7 @@ module SearchProblem = struct
               (ngls, lgls, cost, pptac) :: aux tacl
           with e when CErrors.noncritical e ->
             let e = Exninfo.capture e in
-            Refiner.catch_failerror e; aux tacl
+            Tacticals.catch_failerror e; aux tacl
     in aux l
 
   (* Ordering of states is lexicographic on depth (greatest first) then
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index d1ee55a677..d5358faf59 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -31,7 +31,13 @@ type tactic = Proofview.V82.tac
 
 open Evd
 
-exception FailError = Refiner.FailError
+exception FailError of int * Pp.t Lazy.t
+
+let catch_failerror (e, info) =
+  match e with
+  | FailError (lvl,s) when lvl > 0 ->
+    Exninfo.iraise (FailError (lvl - 1, s), info)
+  | e -> Control.check_for_interrupt ()
 
 let unpackage glsig = (ref (glsig.sigma)), glsig.it
 
@@ -196,7 +202,7 @@ let tclORELSE0 t1 t2 g =
     t1 g
   with (* Breakpoint *)
     | e when CErrors.noncritical e ->
-      let e = Exninfo.capture e in Refiner.catch_failerror e; t2 g
+      let e = Exninfo.capture 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 *)
@@ -209,7 +215,7 @@ let tclORELSE_THEN t1 t2then t2else gls =
   match
     try Some(tclPROGRESS t1 gls)
     with e when CErrors.noncritical e ->
-      let e = Exninfo.capture e in Refiner.catch_failerror e; None
+      let e = Exninfo.capture e in catch_failerror e; None
   with
     | None -> t2else gls
     | Some sgl ->
@@ -464,7 +470,7 @@ module New = struct
       | None -> Exninfo.reify ()
       | Some info -> info
     in
-    tclZERO ~info (Refiner.FailError (lvl,lazy msg))
+    tclZERO ~info (FailError (lvl,lazy msg))
 
   let tclZEROMSG ?info ?loc msg =
     let info = match info with
@@ -482,7 +488,7 @@ module New = struct
 
   let catch_failerror e =
     try
-      Refiner.catch_failerror e;
+      catch_failerror e;
       tclUNIT ()
     with e when CErrors.noncritical e ->
       let _, info = Exninfo.capture e in
@@ -513,7 +519,7 @@ module New = struct
 
   let tclONCE = Proofview.tclONCE
 
-  let tclEXACTLY_ONCE t = Proofview.tclEXACTLY_ONCE (Refiner.FailError(0,lazy (assert false))) t
+  let tclEXACTLY_ONCE t = Proofview.tclEXACTLY_ONCE (FailError(0,lazy (assert false))) t
 
   let tclIFCATCH t tt te =
     tclINDEPENDENT begin
@@ -763,7 +769,7 @@ module New = struct
       begin function (e, info) -> match e with
         | Logic_monad.Tac_Timeout as e ->
           let info = Exninfo.reify () in
-          Proofview.tclZERO ~info (Refiner.FailError (0,lazy (CErrors.print e)))
+          Proofview.tclZERO ~info (FailError (0,lazy (CErrors.print e)))
         | e -> Proofview.tclZERO ~info e
       end
 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 88419af836..48a06e6e1d 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -15,6 +15,13 @@ open Evd
 open Locus
 open Tactypes
 
+(** A special exception for levels for the Fail tactic *)
+exception FailError of int * Pp.t Lazy.t
+
+(** Takes an exception and either raise it at the next
+   level or do nothing. *)
+val catch_failerror  : Exninfo.iexn -> unit
+
 (** Tacticals i.e. functions from tactics to tactics. *)
 
 type tactic = Proofview.V82.tac