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, 3 insertions, 1 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 61d6e0852..aedb81633 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