diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/libobject.ml | 12 | ||||
| -rw-r--r-- | library/summary.ml | 6 |
2 files changed, 6 insertions, 12 deletions
diff --git a/library/libobject.ml b/library/libobject.ml index caa03c85b..8757ca08c 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 6efa07f38..2ec4760d6 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 *) |