aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--proofs/logic.ml1
-rw-r--r--proofs/proof_type.ml3
-rw-r--r--proofs/proof_type.mli7
-rw-r--r--proofs/proofview.ml1
-rw-r--r--proofs/refiner.ml5
-rw-r--r--tactics/class_tactics.ml41
-rw-r--r--tactics/tacinterp.ml18
-rw-r--r--toplevel/cerrors.ml22
-rw-r--r--toplevel/obligations.ml1
9 files changed, 25 insertions, 34 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml
index a0781ae6a..7dc3fb49a 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -57,7 +57,6 @@ let is_unification_error = function
| _ -> false
let rec catchable_exception = function
- | LtacLocated(_,_,e) -> catchable_exception e
| Errors.UserError _ | TypeError _
| RefinerError _ | Indrec.RecursionSchemeError _
| Nametab.GlobalizationError _
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 954e2fdb7..f7f10272c 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -58,5 +58,4 @@ type ltac_call_kind =
type ltac_trace = (int * Loc.t * ltac_call_kind) list
-exception LtacLocated of ltac_trace * Loc.t * exn
-
+let (ltac_trace_info : (ltac_trace * Loc.t) Exninfo.t) = Exninfo.make ()
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 33945052f..74a12d42b 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -73,6 +73,8 @@ type tactic = goal sigma -> goal list sigma
(** Ltac traces *)
+(** TODO: Move those definitions somewhere sensible *)
+
type ltac_call_kind =
| LtacNotationCall of string
| LtacNameCall of ltac_constant
@@ -83,7 +85,4 @@ type ltac_call_kind =
type ltac_trace = (int * Loc.t * ltac_call_kind) list
-(** Invariant: the exceptions embedded in LtacLocated satisfy
- Errors.noncritical *)
-
-exception LtacLocated of ltac_trace * Loc.t * exn
+val ltac_trace_info : (ltac_trace * Loc.t) Exninfo.t
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 1066c173b..96ff63d23 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -334,7 +334,6 @@ let tclEXTEND tacs1 rtac tacs2 env =
this should be maintained synchronized, probably. *)
open Pretype_errors
let rec catchable_exception = function
- | Proof_type.LtacLocated(_,_,e) -> catchable_exception e
| Errors.UserError _
| Type_errors.TypeError _ | PretypeError (_,_,TypingError _)
| Indrec.RecursionSchemeError _
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 5a71b6816..dfc9c0a63 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -216,13 +216,10 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
let catch_failerror e =
if catchable_exception e then check_for_interrupt ()
else match e with
- | FailError (0,_)
- | LtacLocated (_,_,FailError (0,_)) ->
+ | FailError (0,_) ->
check_for_interrupt ()
| FailError (lvl,s) ->
raise (Exninfo.copy e (FailError (lvl - 1, s)))
- | LtacLocated (s'',loc,FailError (lvl,s')) ->
- raise (LtacLocated (s'',loc,FailError (lvl - 1,s')))
| e -> raise e
(** FIXME: do we need to add a [Errors.push] here? *)
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 8da15e8da..84149bead 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -195,7 +195,6 @@ let e_possible_resolve db_list local_db gl =
let rec catchable = function
| Refiner.FailError _ -> true
- | Proof_type.LtacLocated (_, _, e) -> catchable e
| e -> Logic.catchable_exception e
let nb_empty_evars s =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 7ee5a6719..6e2aceaff 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -71,19 +71,21 @@ let dloc = Loc.ghost
let catch_error call_trace tac g =
try tac g with e when Errors.noncritical e ->
let e = Errors.push e in
- let inner_trace,loc,e = match e with
- | LtacLocated (inner_trace,loc,e) -> inner_trace,loc,e
- | e ->
+ let inner_trace,loc,e = match Exninfo.get e ltac_trace_info with
+ | Some (inner_trace,loc) -> inner_trace,loc,e
+ | None ->
let loc = match Loc.get_loc e with
| None -> Loc.ghost
| Some loc -> loc
in
[], loc, e
in
- if List.is_empty call_trace & List.is_empty inner_trace then raise e
+ if List.is_empty call_trace && List.is_empty inner_trace then raise e
else begin
- assert (Errors.noncritical e); (* preserved invariant about LtacLocated *)
- raise (LtacLocated(inner_trace@call_trace,loc,e))
+ assert (Errors.noncritical e); (* preserved invariant *)
+ let new_trace = inner_trace @ call_trace in
+ let located_exc = Exninfo.add e ltac_trace_info (new_trace, loc) in
+ raise located_exc
end
(* Signature for interpretation: val_interp and interpretation functions *)
@@ -1215,12 +1217,10 @@ and eval_with_fail ist is_lazy goal tac =
| a -> a)
with
(** FIXME: Should we add [Errors.push]? *)
- | FailError (0,s) | LtacLocated (_,_,FailError (0,s)) ->
+ | FailError (0,s) ->
raise (Eval_fail (Lazy.force s))
| FailError (lvl,s) as e ->
raise (Exninfo.copy e (FailError (lvl - 1, s)))
- | LtacLocated (s'',loc,FailError (lvl,s')) ->
- raise (LtacLocated (s'',loc,FailError (lvl - 1, s')))
(* Interprets the clauses of a recursive LetIn *)
and interp_letrec ist gl llc u =
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index de4a614c9..d87525bf5 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -57,7 +57,7 @@ let wrap_vernac_error exn strm =
let e = EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None) in
Exninfo.copy exn e
-let rec process_vernac_interp_error exn = match exn with
+let process_vernac_interp_error exn = match exn with
| Univ.UniverseInconsistency (o,u,v,p) ->
let pr_rel r =
match r with
@@ -114,19 +114,19 @@ let rec process_vernac_interp_error exn = match exn with
if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").")
| AlreadyDeclared msg ->
wrap_vernac_error exn (msg ++ str ".")
- | Proof_type.LtacLocated (_,_,(Refiner.FailError (i,s) as exc))
- when not (Pp.is_empty (Lazy.force s)) ->
- (* Ltac error is intended, trace is irrelevant *)
- process_vernac_interp_error exc
- | Proof_type.LtacLocated (s,loc,exc) ->
- let e = process_vernac_interp_error exc in
- assert (Errors.noncritical e);
- (match Himsg.extract_ltac_trace s loc with
- | None,loc -> Loc.add_loc e loc
- | Some msg, loc -> Loc.add_loc (EvaluatedError (msg,Some e)) loc)
| exc ->
exc
+let process_vernac_interp_error exc =
+ let e = process_vernac_interp_error exc in
+ let ltac_trace = Exninfo.get exc Proof_type.ltac_trace_info in
+ match ltac_trace with
+ | None -> e
+ | Some (trace, loc) ->
+ match Himsg.extract_ltac_trace trace loc with
+ | None, loc -> Loc.add_loc e loc
+ | Some msg, loc -> Loc.add_loc (EvaluatedError (msg, Some e)) loc
+
let _ = Tactic_debug.explain_logic_error :=
(fun e -> Errors.print (process_vernac_interp_error e))
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index a369bf505..657973091 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -810,7 +810,6 @@ and solve_obligation_by_tac prg obls i tac =
with e when Errors.noncritical e ->
let e = Errors.push e in
match e with
- | Proof_type.LtacLocated (_, _, Refiner.FailError (_, s))
| Refiner.FailError (_, s) ->
user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
| e -> false
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 15:12:12 +0000