Merge branch 'cerrors-cclosure' into trunk

Was PR#226: CErrors & CClosure

6 files changed, 15 insertions, 15 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 1ea5025397..252b0967dc 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 (*i*)
-open Errors
+open CErrors
 open Util
 open Pp
 open Names
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 0ab1349ecf..917a277c91 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -9,7 +9,7 @@
 open Pp
 open Names
 open Namegen
-open Errors
+open CErrors
 open Util
 open Constrexpr
 open Tacexpr
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 5b73b054dd..0d47b34dfd 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -9,7 +9,7 @@
 open Pp
 open Names
 
-open Errors
+open CErrors
 open Util
 open Extend
 open Vernacexpr
@@ -1082,7 +1082,7 @@ module Make
         )
       | VernacSetOpacity _ ->
         return (
-          Errors.anomaly (keyword "VernacSetOpacity used to set something else")
+          CErrors.anomaly (keyword "VernacSetOpacity used to set something else")
         )
       | VernacSetStrategy l ->
         let pr_lev = function
@@ -1219,7 +1219,7 @@ module Make
 
   let pr_vernac v =
     try pr_vernac_body v ++ sep_end v
-    with e -> Errors.print e
+    with e -> CErrors.print e
 
 end
 
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index ad67becd01..1f6e99c7e7 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -11,7 +11,7 @@
  *)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Nameops
diff --git a/printing/printer.ml b/printing/printer.ml
index 0bac2755b6..28fd92659e 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Term
@@ -184,7 +184,7 @@ let safe_gen f env sigma c =
   let orig_extern_ref = Constrextern.get_extern_reference () in
   let extern_ref loc vars r =
     try orig_extern_ref loc vars r
-    with e when Errors.noncritical e ->
+    with e when CErrors.noncritical e ->
       Libnames.Qualid (loc, qualid_of_global env r)
   in
   Constrextern.set_extern_reference extern_ref;
@@ -192,7 +192,7 @@ let safe_gen f env sigma c =
     let p = f env sigma c in
     Constrextern.set_extern_reference orig_extern_ref;
     p
-  with e when Errors.noncritical e ->
+  with e when CErrors.noncritical e ->
     Constrextern.set_extern_reference orig_extern_ref;
     str "??"
 
@@ -802,13 +802,13 @@ let pr_assumptionset env s =
     in
     let safe_pr_ltype typ =
       try str " : " ++ pr_ltype typ
-      with e when Errors.noncritical e -> mt ()
+      with e when CErrors.noncritical e -> mt ()
     in
     let safe_pr_ltype_relctx (rctx, typ) =
       let sigma, env = get_current_context () in
       let env = Environ.push_rel_context rctx env in
       try str " " ++ pr_ltype_env env sigma typ
-      with e when Errors.noncritical e -> mt ()
+      with e when CErrors.noncritical e -> mt ()
     in
     let pr_axiom env ax typ =
       match ax with
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 5f98eeeab9..c939f54e80 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -254,7 +254,7 @@ let nametab_register_modparam mbid mtb =
        via a Declaremods function that converts back to module entries *)
     try
       Declaremods.process_module_binding mbid (get_typ_expr_alg mtb)
-    with e when Errors.noncritical e ->
+    with e when CErrors.noncritical e ->
       (* Otherwise, we try to play with the nametab ourselves *)
       let mp = MPbound mbid in
       let dir = DirPath.make [MBId.to_id mbid] in
@@ -295,7 +295,7 @@ let print_body is_impl env mp (l,body) =
       try
 	let env = Option.get env in
 	pr_mutual_inductive_body env (MutInd.make2 mp l) mib
-      with e when Errors.noncritical e ->
+      with e when CErrors.noncritical e ->
         let keyword =
           let open Decl_kinds in
           match mib.mind_finite with
@@ -422,7 +422,7 @@ let print_module with_body mp =
   try
     if !short then raise ShortPrinting;
     unsafe_print_module (Some (Global.env ())) mp with_body me ++ fnl ()
-  with e when Errors.noncritical e ->
+  with e when CErrors.noncritical e ->
     unsafe_print_module None mp with_body me ++ fnl ()
 
 let print_modtype kn =
@@ -433,7 +433,7 @@ let print_modtype kn =
      (try
 	if !short then raise ShortPrinting;
 	print_signature' true (Some (Global.env ())) kn mtb.mod_type
-      with e when Errors.noncritical e ->
+      with e when CErrors.noncritical e ->
 	print_signature' true None kn mtb.mod_type))
 
 end