A new mechanism to handle errors.

Instead of the monolitic Cerrors, I introduce a lightweight Errors module
whose error message can be expanded by module introducing exceptions.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14119 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 5 deletions

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index dd48765fb..d98960a48 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -254,14 +254,14 @@ let derive_inversion fix_names =
     with e ->
       msg_warning
 	(str "Cannot built inversion information" ++
-	   if do_observe () then Cerrors.explain_exn e else mt ())
+	   if do_observe () then Errors.print e else mt ())
   with _ -> ()
 
 let warning_error names e =
   let e_explain e =
     match e with
-      | ToShow e -> spc () ++ Cerrors.explain_exn e
-      | _ -> if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()
+      | ToShow e -> spc () ++ Errors.print e
+      | _ -> if do_observe () then (spc () ++ Errors.print e) else mt ()
   in
   match e with
     | Building_graph e ->
@@ -279,8 +279,8 @@ let warning_error names e =
 let error_error names e =
   let e_explain e =
     match e with
-      | ToShow e -> spc () ++ Cerrors.explain_exn e
-      | _ -> if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()
+      | ToShow e -> spc () ++ Errors.print e
+      | _ -> if do_observe () then (spc () ++ Errors.print e) else mt ()
   in
   match e with
     | Building_graph e ->