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

26 files changed, 47 insertions, 46 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 8cbc3ab44..2d1ae68f4 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -907,7 +907,7 @@ let compile fail_on_error ?universes:(universes=0) env c =
       Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
     Some (init_code,!fun_code, Array.of_list fv)
   with TooLargeInductive tname ->
-    let fn = if fail_on_error then Errors.errorlabstrm "compile" else
+    let fn = if fail_on_error then CErrors.errorlabstrm "compile" else
 	       (fun x -> Feedback.msg_warning x) in
       (Pp.(fn
 	   (str "Cannot compile code for virtual machine as it uses inductive " ++
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 817012d8e..04c1bb657 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -19,7 +19,7 @@
 (* This file implements a lazy reduction for the Calculus of Inductive
    Constructions *)
 
-open Errors
+open CErrors
 open Util
 open Pp
 open Names
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 462413bd3..3f1cf9248 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -71,7 +71,7 @@ let set_strategy ({ var_opacity; cst_opacity } as oracle) k l =
     | _ -> Cpred.add c oracle.cst_trstate
     in
     { oracle with cst_opacity; cst_trstate; }
-  | RelKey _ -> Errors.error "set_strategy: RelKey"
+  | RelKey _ -> CErrors.error "set_strategy: RelKey"
 
 let fold_strategy f { var_opacity; cst_opacity; } accu =
   let fvar id lvl accu = f (VarKey id) lvl accu in
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 6dc2a617d..134599150 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -13,7 +13,7 @@
 (* This module implements kernel-level discharching of local
    declarations over global constants and inductive types *)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Term
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 047da682a..acd73d97d 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -224,7 +224,7 @@ and val_of_constr env c =
 	| Some v -> v
 	| None -> assert false
     with reraise ->
-      let reraise = Errors.push reraise in
+      let reraise = CErrors.push reraise in
       let () = print_string "can not compile \n" in
       let () = Format.print_flush () in
       iraise reraise
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 7d8c3c0af..7351a87d4 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -20,7 +20,7 @@
 (* This file defines the type of environments on which the
    type-checker works, together with simple related functions *)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Term
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index e28d770e8..bd91c689d 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Univ
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 0b99c8dc2..de97268b3 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Univ
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 29966facb..7b2d92716 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Univ
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 6fe7e382c..0f0056ed4 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -264,7 +264,7 @@ let add_retroknowledge mp =
     |Retroknowledge.RKRegister (f, e) when (isConst e || isInd e) ->
       Environ.register env f e
     |_ ->
-      Errors.anomaly ~label:"Modops.add_retroknowledge"
+      CErrors.anomaly ~label:"Modops.add_retroknowledge"
         (Pp.str "had to import an unsupported kind of term")
   in
   fun lclrk env ->
diff --git a/kernel/names.ml b/kernel/names.ml
index 9abc9842a..9267a64d6 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -36,7 +36,7 @@ struct
 
   let check_soft ?(warn = true) x =
     let iter (fatal, x) =
-      if fatal then Errors.error x else if warn then Feedback.msg_warning (str x)
+      if fatal then CErrors.error x else if warn then Feedback.msg_warning (str x)
     in
     Option.iter iter (Unicode.ident_refutation x)
 
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 44cf21cff..e2f43b93e 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -5,7 +5,8 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-open Errors
+
+open CErrors
 open Names
 open Term
 open Declarations
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 2f985e15a..3c0afe380 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -5,7 +5,8 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-open Errors
+
+open CErrors
 open Names
 open Nativelib
 open Reduction
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index d4a67b399..1c58c7445 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -8,7 +8,7 @@
 open Util
 open Nativevalues
 open Nativecode
-open Errors
+open CErrors
 open Envars
 
 (** This file provides facilities to access OCaml compiler and dynamic linker,
@@ -125,7 +125,7 @@ let call_linker ?(fatal=true) prefix f upds =
   if not (Sys.file_exists f) then
     begin
       let msg = "Cannot find native compiler file " ^ f in
-      if fatal then Errors.error msg
+      if fatal then CErrors.error msg
       else if !Flags.debug then Feedback.msg_debug (Pp.str msg)
     end
   else
@@ -133,7 +133,7 @@ let call_linker ?(fatal=true) prefix f upds =
     if Dynlink.is_native then Dynlink.loadfile f else !load_obj f;
     register_native_file prefix
    with Dynlink.Error e as exn ->
-     let exn = Errors.push exn in
+     let exn = CErrors.push exn in
      let msg = "Dynlink error, " ^ Dynlink.error_message e in
      if fatal then (Feedback.msg_error (Pp.str msg); iraise exn)
      else if !Flags.debug then Feedback.msg_debug (Pp.str msg));
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index d6fdfefa0..8093df304 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 open Term
 open Names
-open Errors
+open CErrors
 open Util
 
 (** This module defines the representation of values internally used by
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 0c8772d8d..130f1eb03 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -26,10 +26,10 @@ let empty_opaquetab = Int.Map.empty, DirPath.initial
 
 (* hooks *)
 let default_get_opaque dp _ =
-  Errors.error
+  CErrors.error
     ("Cannot access opaque proofs in library " ^ DirPath.to_string dp)
 let default_get_univ dp _ =
-  Errors.error
+  CErrors.error
     ("Cannot access universe constraints of opaque proofs in library " ^
     DirPath.to_string dp)
 
@@ -45,8 +45,8 @@ let create cu = Direct ([],cu)
 let turn_indirect dp o (prfs,odp) = match o with
   | Indirect (_,_,i) ->
       if not (Int.Map.mem i prfs)
-      then Errors.anomaly (Pp.str "Indirect in a different table")
-      else Errors.anomaly (Pp.str "Already an indirect opaque")
+      then CErrors.anomaly (Pp.str "Indirect in a different table")
+      else CErrors.anomaly (Pp.str "Already an indirect opaque")
   | Direct (d,cu) ->
       let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in
       let id = Int.Map.cardinal prfs in
@@ -54,21 +54,21 @@ let turn_indirect dp o (prfs,odp) = match o with
       let ndp =
         if DirPath.equal dp odp then odp
         else if DirPath.equal odp DirPath.initial then dp
-        else Errors.anomaly
+        else CErrors.anomaly
           (Pp.str "Using the same opaque table for multiple dirpaths") in
       Indirect ([],dp,id), (prfs, ndp)
 
 let subst_opaque sub = function
   | Indirect (s,dp,i) -> Indirect (sub::s,dp,i)
-  | Direct _ -> Errors.anomaly (Pp.str "Substituting a Direct opaque")
+  | Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque")
 
 let iter_direct_opaque f = function
-  | Indirect _ -> Errors.anomaly (Pp.str "Not a direct opaque")
+  | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque")
   | Direct (d,cu) ->
       Direct (d,Future.chain ~pure:true cu (fun (c, u) -> f c; c, u))
 
 let discharge_direct_opaque ~cook_constr ci = function
-  | Indirect _ -> Errors.anomaly (Pp.str "Not a direct opaque")
+  | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque")
   | Direct (d,cu) ->
       Direct (ci::d,Future.chain ~pure:true cu (fun (c, u) -> cook_constr c, u))
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 2dc2f0c7c..67b05e526 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -15,7 +15,7 @@
 (* Equal inductive types by Jacek Chrzaszcz as part of the module
    system, Aug 2002 *)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Term
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index fc6155930..23c0c1c31 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -190,7 +190,7 @@ let check_engagement env expected_impredicative_set =
   begin
     match impredicative_set, expected_impredicative_set with
     | PredicativeSet, ImpredicativeSet ->
-        Errors.error "Needs option -impredicative-set."
+        CErrors.error "Needs option -impredicative-set."
     | _ -> ()
   end
 
@@ -344,10 +344,10 @@ let check_required current_libs needed =
     try
       let actual = DPMap.find id current_libs in
       if not(digest_match ~actual ~required) then
-        Errors.error
+        CErrors.error
           ("Inconsistent assumptions over module "^(DirPath.to_string id)^".")
     with Not_found ->
-      Errors.error ("Reference to unknown module "^(DirPath.to_string id)^".")
+      CErrors.error ("Reference to unknown module "^(DirPath.to_string id)^".")
   in
   Array.iter check needed
 
@@ -365,7 +365,7 @@ let safe_push_named d env =
   let _ =
     try
       let _ = Environ.lookup_named id env in
-      Errors.error ("Identifier "^Id.to_string id^" already defined.")
+      CErrors.error ("Identifier "^Id.to_string id^" already defined.")
     with Not_found -> () in
   Environ.push_named d env
 
@@ -815,8 +815,8 @@ let export ?except senv dir =
   let senv =
     try join_safe_environment ?except senv
     with e ->
-      let e = Errors.push e in
-      Errors.errorlabstrm "export" (Errors.iprint e)
+      let e = CErrors.push e in
+      CErrors.errorlabstrm "export" (CErrors.iprint e)
   in
   assert(senv.future_cst = []);
   let () = check_current_library dir senv in
@@ -900,7 +900,7 @@ let register_inline kn senv =
   let open Environ in
   let open Pre_env in
   if not (evaluable_constant kn senv.env) then
-    Errors.error "Register inline: an evaluable constant is expected";
+    CErrors.error "Register inline: an evaluable constant is expected";
   let env = pre_env senv.env in
   let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in
   let cb = {cb with const_inline_code = true} in
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 5efc1078e..c8ceb064d 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -110,7 +110,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   in
   let u = 
     if poly then 
-      Errors.error ("Checking of subtyping of polymorphic" ^
+      CErrors.error ("Checking of subtyping of polymorphic" ^
 		       " inductive types not implemented")
     else Instance.empty
   in
@@ -347,7 +347,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 	      let c2 = Mod_subst.force_constr lc2 in
 	      check_conv NotConvertibleBodyField cst poly u infer_conv env' c1 c2))
    | IndType ((kn,i),mind1) ->
-       ignore (Errors.error (
+       ignore (CErrors.error (
        "The kernel does not recognize yet that a parameter can be " ^
        "instantiated by an inductive type. Hint: you can rename the " ^
        "inductive type and give a definition to map the old name to the new " ^
@@ -364,7 +364,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       let error = NotConvertibleTypeField (env, arity1, typ2) in
        check_conv error cst false Univ.Instance.empty infer_conv_leq env arity1 typ2
    | IndConstr (((kn,i),j) as cstr,mind1) ->
-      ignore (Errors.error (
+      ignore (CErrors.error (
        "The kernel does not recognize yet that a parameter can be " ^
        "instantiated by a constructor. Hint: you can rename the " ^
        "constructor and give a definition to map the old name to the new " ^
diff --git a/kernel/term.ml b/kernel/term.ml
index 4416770fe..15f187e5c 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -8,7 +8,7 @@
 
 open Util
 open Pp
-open Errors
+open CErrors
 open Names
 open Vars
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index be84cae6d..749b5dbaf 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -12,7 +12,7 @@
 (* This module provides the main entry points for type-checking basic
    declarations *)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Term
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 683f6bde5..0059111c0 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Univ
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 00883ddd8..e2712615b 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Pp
-open Errors
 open Util
 open Univ
 
@@ -132,7 +131,7 @@ let change_node g n =
 let rec repr g u =
   let a =
     try UMap.find u g.entries
-    with Not_found -> anomaly ~label:"Univ.repr"
+    with Not_found -> CErrors.anomaly ~label:"Univ.repr"
         (str"Universe " ++ Level.pr u ++ str" undefined")
   in
   match a with
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 126f95f1f..9224ec48d 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -16,7 +16,7 @@
    Sozeau, Pierre-Marie Pédrot *)
 
 open Pp
-open Errors
+open CErrors
 open Util
 
 (* Universes are stratified by a partial ordering $\le$.
diff --git a/kernel/vars.ml b/kernel/vars.ml
index b935ab6b9..2ca749d50 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -173,7 +173,7 @@ let subst_of_rel_context_instance sign l =
     | LocalDef (_,c,_)::sign', args' ->
 	aux (substl subst c :: subst) sign' args'
     | [], [] -> subst
-    | _ -> Errors.anomaly (Pp.str "Instance and signature do not match")
+    | _ -> CErrors.anomaly (Pp.str "Instance and signature do not match")
   in aux [] (List.rev sign) l
 
 let adjust_subst_to_rel_context sign l =
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 702987643..eb992ef89 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -232,7 +232,7 @@ let uni_lvl_val (v : values) : Univ.universe_level =
         | Vatom_stk (a,stk) -> str "Vatom_stk"
         | _ -> assert false
       in
-      Errors.anomaly
+      CErrors.anomaly
         Pp.(   strbrk "Parsing virtual machine value expected universe level, got "
             ++ pr)
 
@@ -282,7 +282,7 @@ let rec whd_accu a stk =
       | _           -> assert false
       end
   | tg ->
-    Errors.anomaly
+    CErrors.anomaly
       Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg)
 
 external kind_of_closure : Obj.t -> int = "coq_kind_of_closure"
@@ -306,7 +306,7 @@ let whd_val : values -> whd =
 	   | 1 -> Vfix(Obj.obj o, None)
 	   | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o))
 	   | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
-	   | _ -> Errors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work"))
+	   | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work"))
 	else
            Vconstr_block(Obj.obj o)