aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/logic_monad.ml14
-rw-r--r--engine/proofview.ml20
-rw-r--r--engine/proofview.mli17
3 files changed, 25 insertions, 26 deletions
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 1caf2c2722..76d98c5ddd 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -89,12 +89,12 @@ struct
let catch = fun s h -> ();
fun () -> try s ()
with Exception e as src ->
- let (src, info) = CErrors.push src in
+ let (src, info) = Exninfo.capture src in
h (e, info) ()
let read_line = fun () -> try read_line () with e ->
- let (e, info) = CErrors.push e in
- raise (e, info) ()
+ let (e, info) = Exninfo.capture e in
+ raise (e,info) ()
let print_char = fun c -> (); fun () -> print_char c
@@ -104,8 +104,8 @@ struct
let make f = (); fun () ->
try f ()
with e when CErrors.noncritical e ->
- let (e, info) = CErrors.push e in
- Util.iraise (Exception e, info)
+ let (e, info) = Exninfo.capture e in
+ Exninfo.iraise (Exception e, info)
(** Use the current logger. The buffer is also flushed. *)
let print_debug s = make (fun _ -> Feedback.msg_debug s)
@@ -115,8 +115,8 @@ struct
let run = fun x ->
try x () with Exception e as src ->
- let (src, info) = CErrors.push src in
- Util.iraise (e, info)
+ let (src, info) = Exninfo.capture src in
+ Exninfo.iraise (e, info)
end
(** {6 Logical layer} *)
diff --git a/engine/proofview.ml b/engine/proofview.ml
index a26ce71141..6a4e490408 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -228,7 +228,7 @@ let apply ~name ~poly env t sp =
let ans = Proof.repr (Proof.run t P.{trace=false; name; poly} (sp,env)) in
let ans = Logic_monad.NonLogical.run ans in
match ans with
- | Nil (e, info) -> iraise (TacticFailure e, info)
+ | Nil (e, info) -> Exninfo.iraise (TacticFailure e, info)
| Cons ((r, (state, _), status, info), _) ->
let (status, gaveup) = status in
let status = (status, state.shelf, gaveup) in
@@ -328,8 +328,8 @@ let tclEXACTLY_ONCE e t =
(** [tclCASE t] wraps the {!Proofview_monad.Logical.split} primitive. *)
type 'a case =
-| Fail of iexn
-| Next of 'a * (iexn -> 'a tactic)
+| Fail of Exninfo.iexn
+| Next of 'a * (Exninfo.iexn -> 'a tactic)
let tclCASE t =
let open Logic_monad in
let map = function
@@ -1096,7 +1096,7 @@ module Goal = struct
let (gl, sigma) = nf_gmake env sigma goal in
tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f gl))
with e when catchable_exception e ->
- let (e, info) = CErrors.push e in
+ let (e, info) = Exninfo.capture e in
tclZERO ~info e
end
end
@@ -1114,7 +1114,7 @@ module Goal = struct
tclEVARMAP >>= fun sigma ->
try f (gmake env sigma goal)
with e when catchable_exception e ->
- let (e, info) = CErrors.push e in
+ let (e, info) = Exninfo.capture e in
tclZERO ~info e
end
end
@@ -1127,7 +1127,7 @@ module Goal = struct
tclEVARMAP >>= fun sigma ->
try f (gmake env sigma goal)
with e when catchable_exception e ->
- let (e, info) = CErrors.push e in
+ let (e, info) = Exninfo.capture e in
tclZERO ~info e
end
| _ ->
@@ -1218,7 +1218,7 @@ module V82 = struct
InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"<unknown>")) >>
Pv.set { ps with solution = evd; comb = sgs; }
with e when catchable_exception e ->
- let (e, info) = CErrors.push e in
+ let (e, info) = Exninfo.capture e in
tclZERO ~info e
@@ -1261,8 +1261,8 @@ module V82 = struct
let (_,final,_,_) = apply ~name ~poly (goal_env env gls.Evd.sigma gls.Evd.it) t init in
{ Evd.sigma = final.solution ; it = CList.map drop_state final.comb }
with Logic_monad.TacticFailure e as src ->
- let (_, info) = CErrors.push src in
- iraise (e, info)
+ let (_, info) = Exninfo.capture src in
+ Exninfo.iraise (e, info)
let put_status = Status.put
@@ -1271,7 +1271,7 @@ module V82 = struct
let wrap_exceptions f =
try f ()
with e when catchable_exception e ->
- let (e, info) = CErrors.push e in tclZERO ~info e
+ let (e, info) = Exninfo.capture e in tclZERO ~info e
end
diff --git a/engine/proofview.mli b/engine/proofview.mli
index a92179ab5b..5bfbc6a649 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -14,7 +14,6 @@
['a tactic] is the (abstract) type of tactics modifying the proof
state and returning a value of type ['a]. *)
-open Util
open EConstr
(** Main state of tactics *)
@@ -194,18 +193,18 @@ val tclZERO : ?info:Exninfo.info -> exn -> 'a tactic
the successes of [t1] have been depleted and it failed with [e],
then it behaves as [t2 e]. In other words, [tclOR] inserts a
backtracking point. *)
-val tclOR : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic
+val tclOR : 'a tactic -> (Exninfo.iexn -> 'a tactic) -> 'a tactic
(** [tclORELSE t1 t2] is equal to [t1] if [t1] has at least one
success or [t2 e] if [t1] fails with [e]. It is analogous to
[try/with] handler of exception in that it is not a backtracking
point. *)
-val tclORELSE : 'a tactic -> (iexn -> 'a tactic) -> 'a tactic
+val tclORELSE : 'a tactic -> (Exninfo.iexn -> 'a tactic) -> 'a tactic
(** [tclIFCATCH a s f] is a generalisation of {!tclORELSE}: if [a]
succeeds at least once then it behaves as [tclBIND a s] otherwise,
if [a] fails with [e], then it behaves as [f e]. *)
-val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (iexn -> 'b tactic) -> 'b tactic
+val tclIFCATCH : 'a tactic -> ('a -> 'b tactic) -> (Exninfo.iexn -> 'b tactic) -> 'b tactic
(** [tclONCE t] behave like [t] except it has at most one success:
[tclONCE t] stops after the first success of [t]. If [t] fails
@@ -227,8 +226,8 @@ val tclEXACTLY_ONCE : exn -> 'a tactic -> 'a tactic
continuation. It is the most general primitive to control
backtracking. *)
type 'a case =
- | Fail of iexn
- | Next of 'a * (iexn -> 'a tactic)
+ | Fail of Exninfo.iexn
+ | Next of 'a * (Exninfo.iexn -> 'a tactic)
val tclCASE : 'a tactic -> 'a case tactic
(** [tclBREAK p t] is a generalization of [tclONCE t]. Instead of
@@ -236,7 +235,7 @@ val tclCASE : 'a tactic -> 'a case tactic
failure with an exception [e] such that [p e = Some e'] is raised. At
which point it drops the remaining successes, failing with [e'].
[tclONCE t] is equivalent to [tclBREAK (fun e -> Some e) t]. *)
-val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic
+val tclBREAK : (Exninfo.iexn -> Exninfo.iexn option) -> 'a tactic -> 'a tactic
(** {7 Focusing tactics} *)
@@ -508,8 +507,8 @@ end
module UnsafeRepr :
sig
type state = Proofview_monad.Logical.Unsafe.state
- val repr : 'a tactic -> ('a, state, state, iexn) Logic_monad.BackState.t
- val make : ('a, state, state, iexn) Logic_monad.BackState.t -> 'a tactic
+ val repr : 'a tactic -> ('a, state, state, Exninfo.iexn) Logic_monad.BackState.t
+ val make : ('a, state, state, Exninfo.iexn) Logic_monad.BackState.t -> 'a tactic
end
(** {6 Goal-dependent tactics} *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:12:21 +0000