From f0341076aa60a84177a6b46db0d8d50df220536b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 6 Dec 2016 17:16:16 +0100
Subject: [error] Move back fatal_error to toplevel

This reverts 4444768d3f4f9c4fcdd440f7ab902886bd8e2b09
(the mllib dependencies that should be surely tweaked more).

The logic for `fatal_error` has no place in `CErrors`, this is
coqtop-specific code.

What is more, a libobject caller should handle the exception correctly,
I fail to see why the fix was needed on the first place.
---
 library/libobject.ml | 12 ++----------
 1 file changed, 2 insertions(+), 10 deletions(-)

(limited to 'library')

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. *)
-- 
cgit v1.2.3


From 3b3d5937939ac8dc4f152d61391630e62bb0b2e5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 7 Dec 2016 12:12:54 +0100
Subject: [pp] [ide] Minor cleanups in pp code.

- We avoid unnecessary use of Pp -> string conversion functions.
  and the creation of intermediate buffers on logging.

- We rename local functions that share the name with the Coq stdlib,
  this is usually dangerous as if the normal function is removed, code
  may pick up the one in the stdlib, with different semantics.
---
 library/summary.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'library')

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 *)
-- 
cgit v1.2.3