Actually adding backtrace handling.

I hope I did not forget some [with] clauses. Otherwise, some
stack frame will be missing from the debug.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16167 85f007b7-540e-0410-9357-904b9bb8a0f7

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