Merge PR#390: Updates to the Pretty Printing Infrastructure

2 files changed, 6 insertions, 12 deletions

diff --git a/library/libobject.ml b/library/libobject.ml
index caa03c85be..8757ca08c6 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -91,16 +91,8 @@ let declare_object_full odecl =
 			     dyn_rebuild_function = rebuild };
   (infun,outfun)
 
-(* The "try .. with .. " allows for correct printing when calling
-   declare_object a loading time.
-*)
-
-let declare_object odecl =
-  try fst (declare_object_full odecl)
-  with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e)
-let declare_object_full odecl =
-  try declare_object_full odecl
-  with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e)
+let declare_object odecl = fst (declare_object_full odecl)
+let declare_object_full odecl = declare_object_full odecl
 
 (* this function describes how the cache, load, open, and export functions
    are triggered. *)
diff --git a/library/summary.ml b/library/summary.ml
index 6efa07f388..2ec4760d64 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -107,8 +107,10 @@ let unfreeze_summaries fs =
     try fold id decl state
     with e when CErrors.noncritical e ->
       let e = CErrors.push e in
-      Printf.eprintf "Error unfrezing summay %s\n%s\n%!"
-        (name_of_summary id) (Pp.string_of_ppcmds (CErrors.iprint e));
+      Feedback.msg_error
+        Pp.(seq [str "Error unfrezing summay %s\n%s\n%!";
+                 str (name_of_summary id);
+                 CErrors.iprint e]);
       iraise e
   in
   (** We rely on the order of the frozen list, and the order of folding *)