aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/safe_typing.ml4
-rw-r--r--library/states.ml1
-rw-r--r--proofs/pfedit.ml1
-rw-r--r--proofs/proofview.ml5
-rw-r--r--tactics/auto.ml2
-rw-r--r--tactics/contradiction.ml36
-rw-r--r--tactics/equality.ml5
-rw-r--r--tactics/tacinterp.ml4
-rw-r--r--tactics/tactics.ml4
-rw-r--r--toplevel/coqloop.ml5
-rw-r--r--toplevel/stm.ml9
-rw-r--r--toplevel/vernacentries.ml5
12 files changed, 44 insertions, 37 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e9be955e8..c89766fb9 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -688,7 +688,9 @@ let export compilation_mode senv dir =
try
if compilation_mode = Flags.BuildVi then { senv with future_cst = [] }
else join_safe_environment senv
- with e -> Errors.errorlabstrm "export" (Errors.print e)
+ with e ->
+ let e = Errors.push e in
+ Errors.errorlabstrm "export" (Errors.print e)
in
assert(senv.future_cst = []);
let () = check_current_library dir senv in
diff --git a/library/states.ml b/library/states.ml
index ea4e7d43c..031222c7d 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -37,6 +37,7 @@ let with_state_protection f x =
try
let a = f x in unfreeze st; a
with reraise ->
+ let reraise = Errors.push reraise in
(unfreeze st; raise reraise)
let with_state_protection_on_exception = Future.transactify
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 68c2ed328..f45eb2a3a 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -126,6 +126,7 @@ let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac
delete_current_proof ();
const, status
with reraise ->
+ let reraise = Errors.push reraise in
delete_current_proof ();
raise reraise
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 055cd14b6..22d908e94 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -723,8 +723,9 @@ module V82 = struct
let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in
let (_,final,_) = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in
{ Evd.sigma = final.solution ; it = final.comb }
- with Proof_errors.TacticFailure e ->
- let e = Errors.push e in
+ with Proof_errors.TacticFailure e as src ->
+ let src = Errors.push src in
+ let e = Backtrace.app_backtrace ~src ~dst:e in
raise e
let put_status b =
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 632f83c83..152556c74 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1205,6 +1205,7 @@ let tclLOG (dbg,depth,trace) pp tac =
msg_debug (str s ++ spc () ++ pp () ++ str ". (*success*)");
out
with reraise ->
+ let reraise = Errors.push reraise in
msg_debug (str s ++ spc () ++ pp () ++ str ". (*fail*)");
raise reraise
end
@@ -1216,6 +1217,7 @@ let tclLOG (dbg,depth,trace) pp tac =
trace := (depth, Some pp) :: !trace;
out
with reraise ->
+ let reraise = Errors.push reraise in
trace := (depth, None) :: !trace;
raise reraise
end
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 9c8412454..f245247a9 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -90,25 +90,23 @@ let contradiction_term (c,lbind as cl) =
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let type_of = Tacmach.New.pf_type_of gl in
- try (* type_of can raise exceptions. *)
- let typ = type_of c in
- let _, ccl = splay_prod env sigma typ in
- if is_empty_type ccl then
- Tacticals.New.tclTHEN (elim false cl None) (Tacticals.New.tclTRY assumption)
- else
- Proofview.tclORELSE
- begin
- if lbind = NoBindings then
- filter_hyp (is_negation_of env sigma typ)
- (fun id -> simplest_elim (mkApp (mkVar id,[|c|])))
- else
- Proofview.tclZERO Not_found
- end
- begin function
- | Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction."))
- | e -> Proofview.tclZERO e
- end
- with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e
+ let typ = type_of c in
+ let _, ccl = splay_prod env sigma typ in
+ if is_empty_type ccl then
+ Tacticals.New.tclTHEN (elim false cl None) (Tacticals.New.tclTRY assumption)
+ else
+ Proofview.tclORELSE
+ begin
+ if lbind = NoBindings then
+ filter_hyp (is_negation_of env sigma typ)
+ (fun id -> simplest_elim (mkApp (mkVar id,[|c|])))
+ else
+ Proofview.tclZERO Not_found
+ end
+ begin function
+ | Not_found -> Proofview.tclZERO (Errors.UserError ("",Pp.str"Not a contradiction."))
+ | e -> Proofview.tclZERO e
+ end
end
let contradiction = function
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 71b3c0045..c59e43b45 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -387,11 +387,6 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
end
begin function
| e ->
- (* Try to see if there's an equality hidden *)
- (* spiwack: [Errors.push] here is unlikely to do
- what it's intended to, or anything meaningful for
- that matter. *)
- let e = Errors.push e in
let env' = push_rel_context rels env in
let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
match match_with_equality_type t' with
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 7c460424e..b3f33b19c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1258,10 +1258,6 @@ and interp_match ist lz constr lmr gl =
(interp_ltac_constr ist constr gl)
begin function
| e ->
- (* spiwack: [Errors.push] here is unlikely to do what
- it's intended to, or anything meaningful for that
- matter. *)
- let e = Errors.push e in
Proofview.tclLIFT (debugging_exception_step ist true e
(fun () -> str "evaluation of the matched expression")) <*>
Proofview.tclZERO e
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9c2a1f6e3..3dd208acb 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3657,11 +3657,13 @@ let abstract_subproof id tac =
let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in
let (const, safe) =
try Pfedit.build_constant_by_tactic id secsign concl solve_tac
- with Proof_errors.TacticFailure e ->
+ with Proof_errors.TacticFailure e as src ->
(* if the tactic [tac] fails, it reports a [TacticFailure e],
which is an error irrelevant to the proof system (in fact it
means that [e] comes from [tac] failing to yield enough
success). Hence it reraises [e]. *)
+ let src = Errors.push src in
+ let e = Backtrace.app_backtrace ~src ~dst:e in
raise e
in
let cd = Entries.DefinitionEntry const in
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index b930c4eec..07a398903 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -290,7 +290,10 @@ let rec discard_to_dot () =
let read_sentence () =
try Vernac.parse_sentence (top_buffer.tokens, None)
- with reraise -> discard_to_dot (); raise reraise
+ with reraise ->
+ let reraise = Errors.push reraise in
+ discard_to_dot ();
+ raise reraise
(** [do_vernac] reads and executes a toplevel phrase, and print error
messages when an exception is raised, except for the following:
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 875c933ef..cc6b7d0c4 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -762,8 +762,9 @@ end = struct (* {{{ *)
{ verbose = false; loc;
expr = (VernacEndProof (Proved (true,None))) };
Some proof
- with e -> (try
- match Stateid.get e with
+ with e ->
+ let e = Errors.push e in
+ (try match Stateid.get e with
| None ->
Pp.pperrnl Pp.(
str"File " ++ str name ++ str ": proof of " ++ str s ++
@@ -891,7 +892,8 @@ end = struct (* {{{ *)
if WorkersPool.is_empty () then
if !Flags.compilation_mode = Flags.BuildVi then begin
let force () : Entries.proof_output list Future.assignement =
- try `Val (build_proof_here_core loc stop ()) with e -> `Exn e in
+ try `Val (build_proof_here_core loc stop ())
+ with e -> let e = Errors.push e in `Exn e in
let f,assign = Future.create_delegate ~force (State.exn_on id ~valid) in
let uuid = Future.uuid f in
TQueue.push queue (TaskBuildProof
@@ -1578,6 +1580,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) =
let u, a, _ = List.fold_left finish_task u (info_tasks tasks) in
(u,a,true), p
with e ->
+ let e = Errors.push e in
Pp.pperrnl Pp.(str"File " ++ str name ++ str ":" ++ spc () ++ print e);
exit 1
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1854e1126..22e2f0c54 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -346,7 +346,10 @@ let dump_universes_gen g s =
Univ.dump_universes output_constraint g;
close ();
msg_info (str ("Universes written to file \""^s^"\"."))
- with reraise -> close (); raise reraise
+ with reraise ->
+ let reraise = Errors.push reraise in
+ close ();
+ raise reraise
let dump_universes sorted s =
let g = Global.universes () in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 11:20:13 +0000