From c44067d1565e7c139c9bde4d041661ac256c3869 Mon Sep 17 00:00:00 2001
From: gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 18 Oct 2013 13:52:05 +0000
Subject: Summary: if an unfreeze function fails, print an error message

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16890 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/summary.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/summary.ml b/library/summary.ml
index af4deb40f..dcc6cce90 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -107,7 +107,11 @@ let unfreeze_summary datas =
   List.iter
     (fun (id, data) ->
       let summary = Hashtbl.find summaries id in
-      summary.unfreeze_function data)
+      try summary.unfreeze_function data
+      with e ->
+        let e = Errors.push e in
+        prerr_endline ("Exception unfreezing " ^ id);
+        raise e)
   datas
 
 (** All-in-one reference declaration + registration *)
-- 
cgit v1.2.3