errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib module)

 For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a

17 files changed, 32 insertions, 32 deletions

diff --git a/library/declare.ml b/library/declare.ml
index f809e9742..3d063225f 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -9,7 +9,7 @@
 (** This module is about the low-level declaration of logical objects *)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Libnames
@@ -149,7 +149,7 @@ let cache_constant ((sp,kn), obj) =
       obj.cst_was_seff <- false;  
       if Global.exists_objlabel (Label.of_id (basename sp))
       then constant_of_kn kn
-      else Errors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp))
+      else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp))
     end else
       let () = check_exists sp in
       let kn', exported = Global.add_constant dir id obj.cst_decl in
diff --git a/library/declaremods.ml b/library/declaremods.ml
index dcd63c769..b2806a1ac 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Declarations
@@ -822,7 +822,7 @@ let protect_summaries f =
   try f fs
   with reraise ->
     (* Something wrong: undo the whole process *)
-    let reraise = Errors.push reraise in
+    let reraise = CErrors.push reraise in
     let () = Summary.unfreeze_summaries fs in
     iraise reraise
 
diff --git a/library/global.ml b/library/global.ml
index c53611931..e748434d2 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -42,7 +42,7 @@ let () =
 
 let assert_not_parsing () =
   if !Flags.we_are_parsing then
-    Errors.anomaly (
+    CErrors.anomaly (
       Pp.strbrk"The global environment cannot be accessed during parsing")
 
 let safe_env () = assert_not_parsing(); !global_env
diff --git a/library/globnames.ml b/library/globnames.ml
index bec463ecf..a78f5f13a 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Names
 open Term
 open Mod_subst
diff --git a/library/goptions.ml b/library/goptions.ml
index 7bead0b63..0459417fb 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -9,7 +9,7 @@
 (* This module manages customization parameters at the vernacular level     *)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Libobject
 open Libnames
diff --git a/library/heads.ml b/library/heads.ml
index 4c9b78976..02465f22f 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -70,7 +70,7 @@ let kind_of_head env t =
   | Const (cst,_) ->
       (try on_subterm k l b (constant_head cst)
        with Not_found ->
-         Errors.anomaly
+         CErrors.anomaly
            Pp.(str "constant not found in kind_of_head: " ++
                str (Names.Constant.to_string cst)))
   | Construct _ | CoFix _ ->
diff --git a/library/impargs.ml b/library/impargs.ml
index 52d5c9c91..6da7e2110 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Globnames
@@ -76,7 +76,7 @@ let with_implicits flags f x =
     implicit_args := oflags;
     rslt
   with reraise ->
-    let reraise = Errors.push reraise in
+    let reraise = CErrors.push reraise in
     let () = implicit_args := oflags in
     iraise reraise
 
diff --git a/library/kindops.ml b/library/kindops.ml
index c634193da..21b1bec33 100644
--- a/library/kindops.ml
+++ b/library/kindops.ml
@@ -25,7 +25,7 @@ let string_of_theorem_kind = function
 
 let string_of_definition_kind def =
   let (locality, poly, kind) = def in
-  let error () = Errors.anomaly (Pp.str "Internal definition kind") in
+  let error () = CErrors.anomaly (Pp.str "Internal definition kind") in
   match kind with
   | Definition ->
     begin match locality with
@@ -64,4 +64,4 @@ let string_of_definition_kind def =
     | Global -> "Global Instance"
     end
   | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) ->
-    Errors.anomaly (Pp.str "Internal definition kind")
+    CErrors.anomaly (Pp.str "Internal definition kind")
diff --git a/library/lib.ml b/library/lib.ml
index 23a2d4846..8880a8b15 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Libnames
 open Globnames
diff --git a/library/libnames.ml b/library/libnames.ml
index 99ff2f2fb..dd74e192f 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 
diff --git a/library/libobject.ml b/library/libobject.ml
index 3e08b38b1..caa03c85b 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -31,7 +31,7 @@ let default_object s = {
   load_function = (fun _ _ -> ());
   open_function = (fun _ _ -> ());
   subst_function = (fun _ ->
-    Errors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!"));
+    CErrors.anomaly (str "The object " ++ str s ++ str " does not know how to substitute!"));
   classify_function = (fun obj -> Keep obj);
   discharge_function = (fun _ -> None);
   rebuild_function = (fun x -> x)}
@@ -97,10 +97,10 @@ let declare_object_full odecl =
 
 let declare_object odecl =
   try fst (declare_object_full odecl)
-  with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e)
+  with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e)
 let declare_object_full odecl =
   try declare_object_full odecl
-  with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e)
+  with e -> CErrors.fatal_error (CErrors.print e) (CErrors.is_anomaly e)
 
 (* this function describes how the cache, load, open, and export functions
    are triggered. *)
diff --git a/library/library.ml b/library/library.ml
index cead90700..12090183a 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 
 open Names
@@ -64,7 +64,7 @@ let fetch_delayed del =
     let () = close_in ch in
     if not (String.equal digest digest') then raise (Faulty f);
     obj
-  with e when Errors.noncritical e -> raise (Faulty f)
+  with e when CErrors.noncritical e -> raise (Faulty f)
 
 end
 
@@ -724,7 +724,7 @@ let save_library_to ?todo dir f otab =
       except Int.Set.empty in
   let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in
   Array.iteri (fun i x ->
-    if not(is_done_or_todo i x) then Errors.errorlabstrm "library"
+    if not(is_done_or_todo i x) then CErrors.errorlabstrm "library"
       Pp.(str"Proof object "++int i++str" is not checked nor to be checked"))
     opaque_table;
   let sd = {
@@ -756,8 +756,8 @@ let save_library_to ?todo dir f otab =
       if not (Nativelib.compile_library dir ast fn) then
 	error "Could not compile the library to native code."
    with reraise ->
-    let reraise = Errors.push reraise in
-    let () = Feedback.msg_notice (str "Removed file " ++ str f') in
+    let reraise = CErrors.push reraise in
+    let () = Feedback.msg_warning (str "Removed file " ++ str f') in
     let () = close_out ch in
     let () = Sys.remove f' in
     iraise reraise
diff --git a/library/loadpath.ml b/library/loadpath.ml
index 6f4d79430..e6f6716c3 100644
--- a/library/loadpath.ml
+++ b/library/loadpath.ml
@@ -8,7 +8,7 @@
 
 open Pp
 open Util
-open Errors
+open CErrors
 open Names
 open Libnames
 
diff --git a/library/nametab.ml b/library/nametab.ml
index f533bc791..fa5db37ed 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Pp
 open Names
diff --git a/library/states.ml b/library/states.ml
index 2e1be764a..95bd819d6 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -35,7 +35,7 @@ let with_state_protection f x =
   try
     let a = f x in unfreeze st; a
   with reraise ->
-    let reraise = Errors.push reraise in
+    let reraise = CErrors.push reraise in
     (unfreeze st; iraise reraise)
 
 let with_state_protection_on_exception = Future.transactify
diff --git a/library/summary.ml b/library/summary.ml
index edea7dbe5..4fef06438 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 
 module Dyn = Dyn.Make(struct end)
@@ -105,10 +105,10 @@ let unfreeze_summaries fs =
   in
   let fold id decl state =
     try fold id decl state
-    with e when Errors.noncritical e ->
-      let e = Errors.push e in
+    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 (Errors.iprint e));
+        (name_of_summary id) (Pp.string_of_ppcmds (CErrors.iprint e));
       iraise e
   in
   (** We rely on the order of the frozen list, and the order of folding *)
@@ -149,7 +149,7 @@ let unfreeze_summary datas =
       let (name, summary) = Int.Map.find id !summaries in
       try summary.unfreeze_function data
       with e ->
-        let e = Errors.push e in
+        let e = CErrors.push e in
         prerr_endline ("Exception unfreezing " ^ name);
         iraise e)
   datas
diff --git a/library/universes.ml b/library/universes.ml
index 21d960ea3..db95607f1 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -112,7 +112,7 @@ let enforce_eq_instances_univs strict x y c =
   let d = if strict then ULub else UEq in
   let ax = Instance.to_array x and ay = Instance.to_array y in
     if Array.length ax != Array.length ay then
-      Errors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++
+      CErrors.anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with" ++
 	       Pp.str " instances of different lengths");
     CArray.fold_right2
       (fun x y -> Constraints.add (Universe.make x, d, Universe.make y))
@@ -337,7 +337,7 @@ let existing_instance ctx inst =
     and a2 = Instance.to_array (UContext.instance ctx) in
     let len1 = Array.length a1 and len2 = Array.length a2 in 
       if not (len1 == len2) then
-	Errors.errorlabstrm "Universes"
+	CErrors.errorlabstrm "Universes"
 	  (str "Polymorphic constant expected " ++ int len2 ++ 
 	     str" levels but was given " ++ int len1)
       else ()