aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/ltac/rewrite.ml4
-rw-r--r--plugins/ltac/tacinterp.ml2
-rw-r--r--proofs/refiner.ml11
-rw-r--r--proofs/refiner.mli7
-rw-r--r--tactics/class_tactics.ml2
-rw-r--r--tactics/eauto.ml2
-rw-r--r--tactics/tacticals.ml20
-rw-r--r--tactics/tacticals.mli7
-rw-r--r--vernac/declare.ml2
-rw-r--r--vernac/himsg.ml2
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) ++
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:04:20 +0000