Move the FailError exception from Refiner to Tacticals.

10 files changed, 27 insertions, 32 deletions

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index f16d0717df..40dea90c00 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1567,7 +1567,7 @@ let assert_replacing id newt tac =
 
 let newfail n s =
   let info = Exninfo.reify () in
-  Proofview.tclZERO ~info (Refiner.FailError (n, lazy s))
+  Proofview.tclZERO ~info (Tacticals.FailError (n, lazy s))
 
 let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
   let open Proofview.Notations in
@@ -1656,7 +1656,7 @@ let cl_rewrite_clause_strat progress strat clause =
       (fun (e, info) -> match e with
        | RewriteFailure e ->
          tclZEROMSG ~info (str"setoid rewrite failed: " ++ e)
-       | Refiner.FailError (n, pp) ->
+       | Tacticals.FailError (n, pp) ->
          tclFAIL ~info n (str"setoid rewrite failed: " ++ Lazy.force pp)
        | e ->
          Proofview.tclZERO ~info e))
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index d65c2f0de9..fdebe14a23 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -22,7 +22,6 @@ open Util
 open Names
 open Nameops
 open Libnames
-open Refiner
 open Tacmach.New
 open Tactic_debug
 open Constrexpr
@@ -1442,6 +1441,7 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } =
     if the left-hand side fails. *)
 and interp_match_successes lz ist s =
    let general =
+     let open Tacticals in
      let break (e, info) = match e with
        | FailError (0, _) -> None
        | FailError (n, s) -> Some (FailError (pred n, s), info)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index cd44b2ae71..b72d544151 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -7,14 +7,3 @@
 (*         *     GNU Lesser General Public License Version 2.1          *)
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
-
-open Util
-
-(* A special exception for levels for the Fail tactic *)
-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 ()
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index e13e358d8f..c38cb23cb0 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -9,10 +9,3 @@
 (************************************************************************)
 
 (** Legacy proof engine. Do not use in newly written code. *)
-
-(** 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
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
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 6326a22e83..85359d5b62 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -2206,7 +2206,7 @@ let solve_by_tac ?loc name evi t ~poly ~uctx =
     Inductiveops.control_only_guard env (Evd.from_ctx uctx) (EConstr.of_constr body);
     Some (body, types, uctx)
   with
-  | Refiner.FailError (_, s) as exn ->
+  | Tacticals.FailError (_, s) as exn ->
     let _ = Exninfo.capture exn in
     CErrors.user_err ?loc ~hdr:"solve_obligation" (Lazy.force s)
   (* If the proof is open we absorb the error and leave the obligation open *)
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 9d67ce3757..79f11fd6bc 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1398,7 +1398,7 @@ let rec vernac_interp_error_handler = function
     str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
     spc () ++ str "was not found" ++
     spc () ++ str "in the current" ++ spc () ++ str "environment."
-  | Refiner.FailError (i,s) ->
+  | Tacticals.FailError (i,s) ->
     let s = Lazy.force s in
     str "Tactic failure" ++
     (if Pp.ismt s then s else str ": " ++ s) ++