aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrintern.ml1
-rw-r--r--interp/notation.ml5
-rw-r--r--kernel/csymtable.ml7
-rw-r--r--lib/errors.ml50
-rw-r--r--lib/errors.mli11
-rw-r--r--lib/flags.ml4
-rw-r--r--lib/pp.ml6
-rw-r--r--lib/system.ml4
-rw-r--r--lib/xml_parser.ml4
-rw-r--r--library/declaremods.ml4
-rw-r--r--library/impargs.ml6
-rw-r--r--library/library.ml11
-rw-r--r--parsing/egramcoq.ml5
-rw-r--r--pretyping/pretyping.ml8
-rw-r--r--proofs/pfedit.ml5
-rw-r--r--tactics/equality.ml1
-rw-r--r--tactics/rewrite.ml41
-rw-r--r--tactics/tacinterp.ml13
-rw-r--r--toplevel/coqinit.ml6
-rw-r--r--toplevel/metasyntax.ml6
-rw-r--r--toplevel/mltop.ml15
-rw-r--r--toplevel/obligations.ml17
-rw-r--r--toplevel/vernac.ml13
-rw-r--r--toplevel/vernacentries.ml9
-rw-r--r--toplevel/vernacinterp.ml1
25 files changed, 159 insertions, 54 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2afd33babb..542ee9857b 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -714,6 +714,7 @@ let intern_applied_reference intern env namedctx lvar args = function
let r,args2 = intern_non_secvar_qualid loc qid intern env lvar args in
find_appl_head_data r, args2
with e ->
+ let e = Errors.push e in
(* Extra allowance for non globalizing functions *)
if !interning_grammar || env.unb then
(GVar (loc,id), [], [], []),args
diff --git a/interp/notation.ml b/interp/notation.ml
index ac71e1ebdc..c55b7b999b 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -928,4 +928,7 @@ let _ =
let with_notation_protection f x =
let fs = freeze () in
try let a = f x in unfreeze fs; a
- with e -> unfreeze fs; raise e
+ with e ->
+ let e = Errors.push e in
+ let () = unfreeze fs in
+ raise e
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 789df8b3d9..bef5b751f0 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -160,7 +160,12 @@ and eval_to_patch env (buff,pl,fv) =
and val_of_constr env c =
let (_,fun_code,_ as ccfv) =
try compile env c
- with e -> print_string "can not compile \n";Format.print_flush();raise e in
+ with e ->
+ let e = Errors.push e in
+ let () = print_string "can not compile \n" in
+ let () = Format.print_flush () in
+ raise e
+ in
eval_to_patch env (to_memory ccfv)
let set_transparent_const kn = () (* !?! *)
diff --git a/lib/errors.ml b/lib/errors.ml
index 342ec10225..e1a8d46b76 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -8,26 +8,35 @@
open Pp
-(* Errors *)
+(** Aliases *)
+
+let push = Backtrace.push_exn
-type backtrace = string option
+let reraise = Backtrace.reraise
-exception Anomaly of string option * std_ppcmds * backtrace (* System errors *)
+(* Errors *)
-let get_backtrace () =
- if !Flags.debug then Some (Printexc.get_backtrace ())
- else None
+exception Anomaly of string option * std_ppcmds * Backtrace.t (* System errors *)
let make_anomaly ?label pp =
- let bt = get_backtrace () in
+ let bt =
+ if !Flags.debug then Backtrace.empty
+ else Backtrace.none
+ in
Anomaly (label, pp, bt)
let anomaly_gen label pp =
- let bt = get_backtrace () in
+ let bt =
+ if !Flags.debug then Backtrace.empty
+ else Backtrace.none
+ in
raise (Anomaly (label, pp, bt))
let anomaly ?loc ?label pp =
- let bt = get_backtrace () in
+ let bt =
+ if !Flags.debug then Backtrace.empty
+ else Backtrace.none
+ in
match loc with
| None -> raise (Anomaly (label, pp, bt))
| Some loc ->
@@ -96,7 +105,10 @@ let raw_anomaly e = match e with
let print_anomaly askreport e =
let bt_info = match e with
- | Anomaly (_, _, Some bt) -> (fnl () ++ hov 0 (str bt))
+ | Anomaly (_, _, Some bt) ->
+ let pr_frame f = str (Backtrace.print_frame f) in
+ let bt = prlist_with_sep fnl pr_frame bt in
+ fnl () ++ hov 0 bt
| _ -> mt ()
in
let info =
@@ -127,3 +139,21 @@ let _ = register_handler begin function
| _ -> raise Unhandled
end
+let rec anomaly_handler = function
+| Anomaly (lbl, pp, bt) ->
+ let bt = Backtrace.push bt in
+ Some (Anomaly (lbl, pp, bt))
+| Loc.Exc_located (loc, e) ->
+ begin match anomaly_handler e with
+ | None -> None
+ | Some e -> Some (Loc.Exc_located (loc, e))
+ end
+| Error_in_file (s, data, e) ->
+ begin match anomaly_handler e with
+ | None -> None
+ | Some e -> Some (Error_in_file (s, data, e))
+ end
+| e -> None
+
+let record_backtrace () =
+ Backtrace.register_backtrace_handler anomaly_handler
diff --git a/lib/errors.mli b/lib/errors.mli
index 00c39c2b3d..d596abb55a 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -11,6 +11,14 @@ open Pp
(** This modules implements basic manipulations of errors for use
throughout Coq's code. *)
+(** {6 Error handling} *)
+
+val push : exn -> exn
+(** Alias for [Backtrace.push_exn]. *)
+
+val reraise : exn -> 'a
+(** Alias for [Backtrace.reraise]. *)
+
(** {6 Generic errors.}
[Anomaly] is used for system errors and [UserError] for the
@@ -85,3 +93,6 @@ val print_no_report : exn -> Pp.std_ppcmds
(** Same as [print], except that anomalies are not printed but re-raised
(used for the Fail command) *)
val print_no_anomaly : exn -> Pp.std_ppcmds
+
+(** Enable registering of backtrace information. *)
+val record_backtrace : unit -> unit
diff --git a/lib/flags.ml b/lib/flags.ml
index 765574cb4b..b4c72b38a1 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -9,12 +9,12 @@
let with_option o f x =
let old = !o in o:=true;
try let r = f x in o := old; r
- with e -> o := old; raise e
+ with e -> o := old; Backtrace.reraise e
let without_option o f x =
let old = !o in o:=false;
try let r = f x in o := old; r
- with e -> o := old; raise e
+ with e -> o := old; Backtrace.reraise e
let boot = ref false
diff --git a/lib/pp.ml b/lib/pp.ml
index b899ef8231..b9dc05edff 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -262,8 +262,10 @@ let pp_dirs ft =
fun (dirstream : _ ppdirs) ->
try
Stream.iter pp_dir dirstream; com_brk ft
- with
- | e -> Format.pp_print_flush ft () ; raise e
+ with e ->
+ let e = Backtrace.push_exn e in
+ let () = Format.pp_print_flush ft () in
+ raise e
(* pretty print on stdout and stderr *)
diff --git a/lib/system.ml b/lib/system.ml
index dbab923af0..ed23bde197 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -142,7 +142,9 @@ let extern_intern ?(warn=true) magic suffix =
marshal_out channel val_0;
close_out channel
with e ->
- begin try_remove filename; raise e end
+ let e = Errors.push e in
+ let () = try_remove filename in
+ raise e
with Sys_error s -> error ("System error: " ^ s)
and intern_state paths name =
try
diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml
index 81fefd8805..108e226783 100644
--- a/lib/xml_parser.ml
+++ b/lib/xml_parser.ml
@@ -166,7 +166,9 @@ let error_of_exn xparser = function
| NoMoreData -> NodeExpected
| Internal_error e -> e
| Xml_lexer.Error e -> convert e
- | e -> raise e
+ | e ->
+ (*let e = Errors.push e in: We do not record backtrace here. *)
+ raise e
let do_parse xparser =
try
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 61d6e08520..aedb816337 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -1006,7 +1006,9 @@ let protect_summaries f =
try f fs
with e ->
(* Something wrong: undo the whole process *)
- Summary.unfreeze_summaries fs; raise e
+ let e = Errors.push e in
+ let () = Summary.unfreeze_summaries fs in
+ raise e
let declare_include interp_struct me_asts =
protect_summaries
diff --git a/library/impargs.ml b/library/impargs.ml
index c8c1ab0058..217169a610 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -75,10 +75,10 @@ let with_implicits flags f x =
let rslt = f x in
implicit_args := oflags;
rslt
- with e -> begin
- implicit_args := oflags;
+ with e ->
+ let e = Errors.push e in
+ let () = implicit_args := oflags in
raise e
- end
let set_maximality imps b =
(* Force maximal insertion on ending implicits (compatibility) *)
diff --git a/library/library.ml b/library/library.ml
index f68a058c23..681a791292 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -371,12 +371,15 @@ let explain_locate_library_error qid = function
| LibNotFound ->
errorlabstrm "load_absolute_library_from"
(str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath")
- | e -> raise e
+ | e ->
+ let e = Errors.push e in
+ raise e
let try_locate_absolute_library dir =
try
locate_absolute_library dir
with e ->
+ let e = Errors.push e in
explain_locate_library_error (qualid_of_dirpath dir) e
let try_locate_qualified_library (loc,qid) =
@@ -384,6 +387,7 @@ let try_locate_qualified_library (loc,qid) =
let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in
dir,f
with e ->
+ let e = Errors.push e in
explain_locate_library_error qid e
@@ -672,7 +676,10 @@ let save_library_to dir f =
| _ -> anomaly (Pp.str "Library compilation failure")
end
with e ->
- msg_warning (str ("Removed file "^f')); close_out ch; Sys.remove f';
+ let e = Errors.push e in
+ let () = msg_warning (str ("Removed file "^f')) in
+ let () = close_out ch in
+ let () = Sys.remove f' in
raise e
(************************************************************************)
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 4fc251edc0..a53bf630ed 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -341,4 +341,7 @@ let _ =
let with_grammar_rule_protection f x =
let fs = freeze () in
try let a = f x in unfreeze fs; a
- with e -> unfreeze fs; raise e
+ with e ->
+ let e = Errors.push e in
+ let () = unfreeze fs in
+ raise e
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index bcabf1cd98..ed087fa255 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -69,7 +69,7 @@ let search_guard loc env possible_indexes fixdefs =
let indexes = Array.of_list (List.map List.hd possible_indexes) in
let fix = ((indexes, 0),fixdefs) in
(try check_fix env fix with
- | e -> Loc.raise loc e);
+ | e -> let e = Errors.push e in Loc.raise loc e);
indexes
else
(* we now search recursively amoungst all combinations *)
@@ -114,7 +114,7 @@ let resolve_evars env evdref fail_evar resolve_classes =
(* Resolve eagerly, potentially making wrong choices *)
evdref := (try consider_remaining_unif_problems
~ts:(Typeclasses.classes_transparent_state ()) env !evdref
- with e -> if fail_evar then raise e else !evdref)
+ with e -> let e = Errors.push e in if fail_evar then raise e else !evdref)
let solve_remaining_evars fail_evar use_classes hook env initial_sigma (evd,c) =
let evdref = ref evd in
@@ -362,7 +362,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
| GCoFix i ->
let cofix = (i,(names,ftys,fdefs)) in
- (try check_cofix env cofix with e -> Loc.raise loc e);
+ (try check_cofix env cofix with e -> let e = Errors.push e in Loc.raise loc e);
make_judge (mkCoFix cofix) ftys.(i) in
inh_conv_coerce_to_tycon loc env evdref fixj tycon
@@ -473,7 +473,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
in
let resj =
try judge_of_product env name j j'
- with TypeError _ as e -> Loc.raise loc e in
+ with TypeError _ as e -> let e = Errors.push e in Loc.raise loc e in
inh_conv_coerce_to_tycon loc env evdref resj tycon
| GLetIn(loc,name,c1,c2) ->
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index ef92e8e427..961ff41fb7 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -55,7 +55,10 @@ let start_proof id str hyps c ?init_tac ?compute_guard hook =
| None -> Proofview.tclUNIT ()
in
try Proof_global.run_tactic tac
- with e -> Proof_global.discard_current (); raise e
+ with e ->
+ let e = Errors.push e in
+ Proof_global.discard_current ();
+ raise e
let restart_proof () = undo_todepth 1
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 226f0c20f1..08c6ef4a1d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -334,6 +334,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
rewrite_side_tac (!general_rewrite_clause cls
lft2rgt occs (c,l) ~new_goals:[]) tac gl
with e -> (* Try to see if there's an equality hidden *)
+ 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/rewrite.ml4 b/tactics/rewrite.ml4
index cc4b9d3924..6b2f02f411 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1984,6 +1984,7 @@ let setoid_proof gl ty fn fallback =
with e ->
try fallback gl
with Hipattern.NoEquationFound ->
+ let e = Errors.push e in
match e with
| Not_found ->
let rel, args = decompose_app_rel env (project gl) (pf_concl gl) in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 730be93030..9ce5cbf328 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -70,9 +70,11 @@ let dloc = Loc.ghost
let catch_error call_trace tac g =
if List.is_empty call_trace then tac g else try tac g with
- | LtacLocated _ as e -> raise e
- | Loc.Exc_located (_,LtacLocated _) as e -> raise e
+ | LtacLocated _ as e -> let e = Errors.push e in raise e
+ | Loc.Exc_located (_,LtacLocated _) as e ->
+ let e = Errors.push e in raise e
| e ->
+ let e = Errors.push e in
let (nrep,loc',c),tail = List.sep_last call_trace in
let loc,e' = match e with Loc.Exc_located(loc,e) -> loc,e | _ ->dloc,e in
if List.is_empty tail then
@@ -618,6 +620,7 @@ let interp_may_eval f ist gl = function
try
f ist gl c
with e ->
+ let e = Errors.push e in
debugging_exception_step ist false e (fun () ->
str"interpretation of term " ++ pr_glob_constr_env (pf_env gl) (fst c));
raise e
@@ -628,6 +631,7 @@ let interp_constr_may_eval ist gl c =
try
interp_may_eval pf_interp_constr ist gl c
with e ->
+ let e = Errors.push e in
debugging_exception_step ist false e (fun () -> str"evaluation of term");
raise e
in
@@ -1143,6 +1147,7 @@ and interp_app loc ist gl fv largs =
catch_error trace
(val_interp {ist with lfun=newlfun@olfun; trace=trace} gl) body
with e ->
+ let e = Errors.push e in
debugging_exception_step ist false e (fun () -> str "evaluation");
raise e in
let gl = { gl with sigma=sigma } in
@@ -1434,6 +1439,7 @@ and interp_match ist g lz constr lmr =
let lmatch =
try extended_matches c csr
with e ->
+ let e = Errors.push e in
debugging_exception_step ist false e (fun () ->
str "matching with pattern" ++ fnl () ++
pr_constr_pattern_env (pf_env g) c);
@@ -1442,6 +1448,7 @@ and interp_match ist g lz constr lmr =
let lfun = extend_values_with_bindings lmatch ist.lfun in
eval_with_fail { ist with lfun=lfun } lz g mt
with e ->
+ let e = Errors.push e in
debugging_exception_step ist false e (fun () ->
str "rule body for pattern" ++
pr_constr_pattern_env (pf_env g) c);
@@ -1458,12 +1465,14 @@ and interp_match ist g lz constr lmr =
"No matching clauses for match.") in
let (sigma,csr) =
try interp_ltac_constr ist g constr with e ->
+ let e = Errors.push e in
debugging_exception_step ist true e
(fun () -> str "evaluation of the matched expression");
raise e in
let ilr = read_match_rule (fst (extract_ltac_constr_values ist (pf_env g))) ist (pf_env g) sigma lmr in
let res =
try apply_match ist sigma csr ilr with e ->
+ let e = Errors.push e in
debugging_exception_step ist true e (fun () -> str "match expression");
raise e in
debugging_step ist (fun () ->
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index b4d0bc4134..525a924ed9 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -13,6 +13,7 @@ let (/) = Filename.concat
let set_debug () =
let () = Printexc.record_backtrace true in
+ let () = Errors.record_backtrace () in
Flags.debug := true
(* Loading of the ressource file.
@@ -51,8 +52,9 @@ let load_rcfile() =
" found. Skipping rcfile loading."))
*)
with e ->
- (msg_info (str"Load of rcfile failed.");
- raise e)
+ let e = Errors.push e in
+ let () = msg_info (str"Load of rcfile failed.") in
+ raise e
else
Flags.if_verbose msg_info (str"Skipping rcfile loading.")
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a785dd31a4..1e41cdec8f 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -267,6 +267,7 @@ let parse_format ((loc, str) : lstring) =
else
error "Empty format."
with e ->
+ let e = Errors.push e in
Loc.raise loc e
(***********************)
@@ -1072,7 +1073,10 @@ let inNotation : notation_obj -> obj =
let with_lib_stk_protection f x =
let fs = Lib.freeze () in
try let a = f x in Lib.unfreeze fs; a
- with e -> Lib.unfreeze fs; raise e
+ with e ->
+ let e = Errors.push e in
+ let () = Lib.unfreeze fs in
+ raise e
let with_syntax_protection f x =
with_lib_stk_protection
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 4ac6adc354..59059a77af 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -117,12 +117,15 @@ let dir_ml_load s =
| WithTop t ->
(try t.load_obj s
with
- | (UserError _ | Failure _ | Not_found as u) -> raise u
- | u when Errors.is_anomaly u -> raise u
- | exc ->
- let msg = report_on_load_obj_error exc in
- errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++
- str s ++ str" to Coq code (" ++ msg ++ str ")."))
+ | e ->
+ let e = Errors.push e in
+ match e with
+ | (UserError _ | Failure _ | Not_found as u) -> raise u
+ | u when is_anomaly u -> reraise u
+ | exc ->
+ let msg = report_on_load_obj_error exc in
+ errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++
+ str s ++ str" to Coq code (" ++ msg ++ str ")."))
| WithoutTop ->
let warn = Flags.is_verbose() in
let _,gname = find_file_in_path ~warn !coq_mlpath_copy s in
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 68dfca9f93..6ec01f5474 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -736,6 +736,7 @@ let solve_by_tac evi t =
const.Entries.const_entry_body;
const.Entries.const_entry_body
with e ->
+ let e = Errors.push e in
Pfedit.delete_current_proof();
raise e
@@ -818,13 +819,15 @@ and solve_obligation_by_tac prg obls i tac =
obls.(i) <- declare_obligation prg obl t;
true
else false
- with
- | Loc.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
- | Loc.Exc_located(_, Refiner.FailError (_, s))
- | Refiner.FailError (_, s) ->
- user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
- | e when Errors.is_anomaly e -> raise e
- | e -> false
+ with e ->
+ let e = Errors.push e in
+ match e with
+ | Loc.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
+ | Loc.Exc_located(_, Refiner.FailError (_, s))
+ | Refiner.FailError (_, s) ->
+ user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
+ | e when is_anomaly e -> raise e
+ | e -> false
and solve_prg_obligations prg ?oblset tac =
let obls, rem = prg.prg_obligations in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 7a17a2b31e..cb8962a9b9 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -284,6 +284,7 @@ let rec vernac_com interpfun checknav (loc,com) =
restore_translator_coqdoc st;
status
with e ->
+ let e = Errors.push e in
restore_translator_coqdoc st;
raise e
end
@@ -298,7 +299,9 @@ let rec vernac_com interpfun checknav (loc,com) =
(* If the command actually works, ignore its effects on the state *)
States.with_state_protection
(fun v -> ignore (interp v); raise HasNotFailed) v
- with e -> match real_error e with
+ with e ->
+ let e = Errors.push e in
+ match real_error e with
| HasNotFailed ->
errorlabstrm "Fail" (str "The command has not failed !")
| e ->
@@ -331,7 +334,10 @@ let rec vernac_com interpfun checknav (loc,com) =
in
restore_timeout psh;
status
- with e -> restore_timeout psh; raise e
+ with e ->
+ let e = Errors.push e in
+ restore_timeout psh;
+ raise e
in
try
checknav loc com;
@@ -341,6 +347,7 @@ let rec vernac_com interpfun checknav (loc,com) =
let com = if !time then VernacTime com else com in
interp com
with e ->
+ let e = Errors.push e in
Format.set_formatter_out_channel stdout;
raise (DuringCommandInterp (loc, e))
@@ -375,6 +382,7 @@ and read_vernac_file verbosely s =
done;
assert false
with e -> (* whatever the exception *)
+ let e = Errors.push e in
Format.set_formatter_out_channel stdout;
close_input in_chan input; (* we must close the file first *)
match real_error e with
@@ -420,6 +428,7 @@ let load_vernac verb file =
let _ = read_vernac_file verb file in
if !Flags.beautify_file then close_out !chan_beautify;
with e ->
+ let e = Errors.push e in
if !Flags.beautify_file then close_out !chan_beautify;
raise_with_file file e
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7e681b1a08..8fb3aa66b6 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1791,11 +1791,12 @@ let interp c =
interp c; Locality.check_locality ();
Flags.program_mode := mode;
true
- with
+ with e ->
+ let e = Errors.push e in
+ match e with
| UnsafeSuccess ->
Flags.program_mode := mode;
false
| e ->
- Flags.program_mode := mode;
- raise e
-
+ Flags.program_mode := mode;
+ raise e
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index dca47f7146..fdfa514278 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -55,6 +55,7 @@ let call (opn,converted_args) =
with
| Drop -> raise Drop
| e ->
+ let e = Errors.push e in
if !Flags.debug then
msg_debug (str"Vernac Interpreter " ++ str !loc);
raise e
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:04:40 +0000