Merge branch 'cerrors-cclosure' into trunk

Was PR#226: CErrors & CClosure

28 files changed, 79 insertions, 79 deletions

diff --git a/kernel/closure.ml b/kernel/cClosure.ml
index 817012d8ec..d475f097ce 100644
--- a/kernel/closure.ml
+++ b/kernel/cClosure.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
@@ -154,7 +154,7 @@ module RedFlags = (struct
     | ETA -> { red with r_eta = false }
     | DELTA -> { red with r_delta = false }
     | CONST kn ->
- 	let (l1,l2) = red.r_const in
+	let (l1,l2) = red.r_const in
 	{ red with r_const = l1, Cpred.remove kn l2 }
     | MATCH -> { red with r_match = false }
     | FIX -> { red with r_fix = false }
@@ -187,7 +187,7 @@ module RedFlags = (struct
     | DELTA -> (* Used for Rel/Var defined in context *)
 	incr_cnt red.r_delta delta
 
-  let red_projection red p = 
+  let red_projection red p =
     if Projection.unfolded p then true
     else red_set red (fCONST (Projection.constant p))
 
@@ -238,7 +238,7 @@ type table_key = constant puniverses tableKey
 
 let eq_pconstant_key (c,u) (c',u') =
   eq_constant_key c c' && Univ.Instance.equal u u'
-  
+
 module IdKeyHash =
 struct
   open Hashset.Combine
@@ -261,7 +261,7 @@ type 'a infos_cache = {
   i_rels : constr option array;
   i_tab : 'a KeyTable.t }
 
-and 'a infos = { 
+and 'a infos = {
   i_flags : reds;
   i_cache : 'a infos_cache }
 
@@ -320,7 +320,7 @@ let defined_rels flags env =
 (*  else (0,[])*)
 
 let create mk_cl flgs env evars =
-  let cache = 
+  let cache =
     { i_repr = mk_cl;
       i_env = env;
       i_sigma = evars;
@@ -670,7 +670,7 @@ let rec zip m stk =
     | ZcaseT(ci,p,br,e)::s ->
         let t = FCaseT(ci, p, m, br, e) in
         zip {norm=neutr m.norm; term=t} s
-    | Zproj (i,j,cst) :: s -> 
+    | Zproj (i,j,cst) :: s ->
         zip {norm=neutr m.norm; term=FProj(Projection.make cst true,m)} s
     | Zfix(fx,par)::s ->
         zip fx (par @ append_stack [|m|] s)
@@ -777,7 +777,7 @@ let rec try_drop_parameters depth n argstk =
           let aft = Array.sub args n (q-n) in
           reloc_rargs depth (append_stack aft s)
     | Zshift(k)::s -> try_drop_parameters (depth-k) n s
-    | [] -> 
+    | [] ->
 	if Int.equal n 0 then []
 	else raise Not_found
     | _ -> assert false
@@ -786,23 +786,23 @@ let rec try_drop_parameters depth n argstk =
 let drop_parameters depth n argstk =
   try try_drop_parameters depth n argstk
   with Not_found ->
-  (* we know that n < stack_args_size(argstk) (if well-typed term) *) 
+  (* we know that n < stack_args_size(argstk) (if well-typed term) *)
   anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor")
 
 (** [eta_expand_ind_stack env ind c s t] computes stacks corresponding
-    to the conversion of the eta expansion of t, considered as an inhabitant 
+    to the conversion of the eta expansion of t, considered as an inhabitant
     of ind, and the Constructor c of this inductive type applied to arguments
     s.
     @assumes [t] is an irreducible term, and not a constructor. [ind] is the inductive
-    of the constructor term [c] 
-    @raises Not_found if the inductive is not a primitive record, or if the 
+    of the constructor term [c]
+    @raises Not_found if the inductive is not a primitive record, or if the
     constructor is partially applied.
  *)
 let eta_expand_ind_stack env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
     | Some (Some (_,projs,pbs)) when
-	mib.Declarations.mind_finite == Decl_kinds.BiFinite -> 
+	mib.Declarations.mind_finite == Decl_kinds.BiFinite ->
 	(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
 	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
       let pars = mib.Declarations.mind_nparams in
@@ -812,12 +812,12 @@ let eta_expand_ind_stack env ind m s (f, s') =
       let argss = try_drop_parameters depth pars args in
       let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
 					 term = FProj (Projection.make p true, right) }) projs in
-	argss, [Zapp hstack]	
+	argss, [Zapp hstack]
     | _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
 
 let rec project_nth_arg n argstk =
   match argstk with
-  | Zapp args :: s -> 
+  | Zapp args :: s ->
       let q = Array.length args in
 	if n >= q then project_nth_arg (n - q) s
 	else (* n < q *) args.(n)
@@ -872,7 +872,7 @@ let rec knh info m stk =
           (match try Some (lookup_projection p (info_env info)) with Not_found -> None with
 	  | None -> (m, stk)
 	  | Some pb ->
-	     knh info c (Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, 
+	     knh info c (Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg,
 				Projection.constant p)
 			 :: zupdate m stk))
 	else (m,stk)
@@ -974,8 +974,8 @@ let rec zip_term zfun m stk =
         let t = mkCase(ci, zfun (mk_clos e p), m,
 		       Array.map (fun b -> zfun (mk_clos e b)) br) in
         zip_term zfun t s
-    | Zproj(_,_,p)::s -> 
-        let t = mkProj (Projection.make p true, m) in 
+    | Zproj(_,_,p)::s ->
+        let t = mkProj (Projection.make p true, m) in
 	zip_term zfun t s
     | Zfix(fx,par)::s ->
         let h = mkApp(zip_term zfun (zfun fx) par,[|m|]) in
@@ -1055,18 +1055,17 @@ let oracle_of_infos infos = Environ.oracle infos.i_cache.i_env
 
 let env_of_infos infos = infos.i_cache.i_env
 
-let infos_with_reds infos reds = 
+let infos_with_reds infos reds =
   { infos with i_flags = reds }
 
-let unfold_reference info key = 
+let unfold_reference info key =
   match key with
   | ConstKey (kn,_) ->
     if red_set info.i_flags (fCONST kn) then
-      ref_value_cache info key  
+      ref_value_cache info key
     else None
-  | VarKey i -> 
+  | VarKey i ->
     if red_set info.i_flags (fVAR i) then
       ref_value_cache info key
     else None
   | _ -> ref_value_cache info key
-  
diff --git a/kernel/closure.mli b/kernel/cClosure.mli
index 76145e3f80..077756ac74 100644
--- a/kernel/closure.mli
+++ b/kernel/cClosure.mli
@@ -66,7 +66,7 @@ module type RedFlagsSig = sig
 
   (** Tests if a reduction kind is set *)
   val red_set : reds -> red_kind -> bool
-    
+
   (** This tests if the projection is in unfolded state already or
       is unfodable due to delta. *)
   val red_projection : reds -> projection -> bool
@@ -95,7 +95,7 @@ val unfold_red : evaluable_global_reference -> reds
 type table_key = constant puniverses tableKey
 
 type 'a infos_cache
-type 'a infos = { 
+type 'a infos = {
   i_flags : reds;
   i_cache : 'a infos_cache }
 
@@ -204,16 +204,16 @@ val whd_val : clos_infos -> fconstr -> constr
 val whd_stack :
   clos_infos -> fconstr -> stack -> fconstr * stack
 
-(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding 
-    to the conversion of the eta expansion of t, considered as an inhabitant 
+(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding
+    to the conversion of the eta expansion of t, considered as an inhabitant
     of ind, and the Constructor c of this inductive type applied to arguments
     s.
     @assumes [t] is a rigid term, and not a constructor. [ind] is the inductive
-    of the constructor term [c] 
-    @raises Not_found if the inductive is not a primitive record, or if the 
+    of the constructor term [c]
+    @raises Not_found if the inductive is not a primitive record, or if the
     constructor is partially applied.
  *)
-val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> 
+val eta_expand_ind_stack : env -> inductive -> fconstr -> stack ->
    (fconstr * stack) -> stack * stack
 
 (** Conversion auxiliary functions to do step by step normalisation *)
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 8cbc3ab445..2d1ae68f4b 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/conv_oracle.ml b/kernel/conv_oracle.ml
index 462413bd38..3f1cf92487 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 6dc2a617dd..1345991503 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 047da682ad..acd73d97d7 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 7d8c3c0af6..7351a87d44 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 e28d770e8b..bd91c689d2 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 0b99c8dc23..de97268b37 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 29966facbf..7b2d927162 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/kernel.mllib b/kernel/kernel.mllib
index 1e132e3ab2..15f213ce9c 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -25,7 +25,7 @@ Nativelambda
 Nativecode
 Nativelib
 Environ
-Closure
+CClosure
 Reduction
 Nativeconv
 Type_errors
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 6fe7e382c6..0f0056ed43 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 9abc9842a8..9267a64d61 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 44cf21cff0..e2f43b93ee 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 2f985e15ac..3c0afe3805 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 d4a67b3999..1c58c7445c 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 d6fdfefa02..8093df3044 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 0c8772d8d2..130f1eb039 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 2dc2f0c7c9..6c664f7918 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -15,13 +15,13 @@
 (* Equal inductive types by Jacek Chrzaszcz as part of the module
    system, Aug 2002 *)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Term
 open Vars
 open Environ
-open Closure
+open CClosure
 open Esubst
 open Context.Rel.Declaration
 
@@ -318,7 +318,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	   convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
        with NotConvertible ->
            (* else the oracle tells which constant is to be expanded *)
-	 let oracle = Closure.oracle_of_infos infos in
+	 let oracle = CClosure.oracle_of_infos infos in
          let (app1,app2) =
            if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then
 	     match unfold_reference infos fl1 with
@@ -537,7 +537,7 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
   else raise NotConvertible
 
 let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
-  let reds = Closure.RedFlags.red_add_transparent betaiotazeta trans in
+  let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
   let infos = create_clos_infos ~evars reds env in
   ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index fc61559301..23c0c1c31b 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 5efc1078ee..c8ceb064d5 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 4416770fe4..15f187e5c4 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 be84cae6da..749b5dbafa 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 683f6bde55..0059111c09 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 00883ddd84..e2712615be 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 126f95f1f1..9224ec48d7 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 b935ab6b91..2ca749d505 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 7029876438..eb992ef892 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)