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

1 files changed, 5 insertions, 1 deletions

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