aboutsummaryrefslogtreecommitdiff
path: root/engine/proofview.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/proofview.ml')
-rw-r--r--engine/proofview.ml62
1 files changed, 32 insertions, 30 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 6f8e668e4e..2e036be9e3 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -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
@@ -262,6 +262,8 @@ module Monad = Proof
(** [tclZERO e] fails with exception [e]. It has no success. *)
let tclZERO ?info e =
+ if not (CErrors.noncritical e) then
+ CErrors.anomaly (Pp.str "tclZERO receiving critical error: " ++ CErrors.print e);
let info = match info with
| None -> Exninfo.null
| Some info -> info
@@ -302,8 +304,9 @@ let tclONCE = Proof.once
exception MoreThanOneSuccess
let _ = CErrors.register_handler begin function
- | MoreThanOneSuccess -> CErrors.user_err Pp.(str "This tactic has more than one success.")
- | _ -> raise CErrors.Unhandled
+ | MoreThanOneSuccess ->
+ Some (Pp.str "This tactic has more than one success.")
+ | _ -> None
end
(** [tclEXACTLY_ONCE e t] succeeds as [t] if [t] has exactly one
@@ -327,8 +330,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
@@ -347,9 +350,8 @@ exception NoSuchGoals of int
let _ = CErrors.register_handler begin function
| NoSuchGoals n ->
- CErrors.user_err
- (str "No such " ++ str (String.plural n "goal") ++ str ".")
- | _ -> raise CErrors.Unhandled
+ Some (str "No such " ++ str (String.plural n "goal") ++ str ".")
+ | _ -> None
end
(** [tclFOCUS ?nosuchgoal i j t] applies [t] in a context where
@@ -420,13 +422,11 @@ let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t =
exception SizeMismatch of int*int
let _ = CErrors.register_handler begin function
| SizeMismatch (i,j) ->
- let open Pp in
- let errmsg =
- str"Incorrect number of goals" ++ spc() ++
- str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str")."
- in
- CErrors.user_err errmsg
- | _ -> raise CErrors.Unhandled
+ let open Pp in
+ Some (
+ str"Incorrect number of goals" ++ spc() ++
+ str"(expected "++int i++str(String.plural i " tactic") ++ str", was given "++ int j++str").")
+ | _ -> None
end
(** A variant of [Monad.List.iter] where we iter over the focused list
@@ -910,8 +910,9 @@ let tclPROGRESS t =
tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS", Pp.str "Failed to progress."))
let _ = CErrors.register_handler begin function
- | Logic_monad.Tac_Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
- | _ -> raise CErrors.Unhandled
+ | Logic_monad.Tac_Timeout ->
+ Some (Pp.str "[Proofview.tclTIMEOUT] Tactic timeout!")
+ | _ -> None
end
let tclTIMEOUT n t =
@@ -939,7 +940,7 @@ let tclTIMEOUT n t =
return (Util.Inr (Logic_monad.Tac_Timeout, info))
| Logic_monad.TacticFailure e ->
return (Util.Inr (e, info))
- | e -> Logic_monad.NonLogical.raise ~info e
+ | e -> Logic_monad.NonLogical.raise (e, info)
end
end >>= function
| Util.Inl (res,s,m,i) ->
@@ -1039,9 +1040,9 @@ let (>>=) = tclBIND
(** {6 Goal-dependent tactics} *)
-let goal_env evars gl =
+let goal_env env evars gl =
let evi = Evd.find evars gl in
- Evd.evar_filtered_env evi
+ Evd.evar_filtered_env env evi
let goal_nf_evar sigma gl =
let evi = Evd.find sigma gl in
@@ -1097,7 +1098,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
@@ -1115,7 +1116,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
@@ -1128,7 +1129,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
| _ ->
@@ -1219,7 +1220,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
@@ -1256,13 +1257,14 @@ module V82 = struct
let of_tactic t gls =
try
+ let env = Global.env () in
let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in
let name, poly = Names.Id.of_string "legacy_pe", false in
- let (_,final,_,_) = apply ~name ~poly (goal_env gls.Evd.sigma gls.Evd.it) t init in
+ 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 +1273,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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 18:07:20 +0000