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

3 files changed, 15 insertions, 6 deletions

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
 
 (************************************************************************)