Merge branch 'cerrors-cclosure' into trunk

Was PR#226: CErrors & CClosure

29 files changed, 103 insertions, 103 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c39a57012b..985ad4b0d3 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Nameops
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 1321474871..84bf849e76 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -10,7 +10,7 @@ open Util
 open Names
 open Term
 open Vars
-open Closure
+open CClosure
 open Esubst
 
 (**** Call by value reduction ****)
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index de37d1fc5e..87a03abbd9 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -9,7 +9,7 @@
 open Names
 open Term
 open Environ
-open Closure
+open CClosure
 open Esubst
 
 (***********************************************************************
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 5fb6c130eb..4f265e76c9 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Pp
 open Flags
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 704559dd73..913e80f399 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -14,7 +14,7 @@
    Corbineau, Feb 2008 *)
 (* Turned into an abstract compilation unit by Matthieu Sozeau, March 2006 *)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Term
@@ -370,7 +370,7 @@ let apply_coercion env sigma p hj typ_cl =
       (hj,typ_cl,sigma) p
     in evd, j
   with NoCoercion as e -> raise e
-  | e when Errors.noncritical e -> anomaly (Pp.str "apply_coercion")
+  | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion")
 
 (* Try to coerce to a funclass; raise NoCoercion if not possible *)
 let inh_app_fun_core env evd j =
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index c566839e85..886a982634 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -8,7 +8,7 @@
 
 (*i*)
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Globnames
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index cc178eb975..d4066f387b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Term
@@ -323,7 +323,7 @@ let is_nondep_branch c l =
     (* FIXME: do better using tags from l *)
     let sign,ccl = decompose_lam_n_decls (List.length l) c in
     noccur_between 1 (Context.Rel.length sign) ccl
-  with e when Errors.noncritical e -> (* Not eta-expanded or not reduced *)
+  with e when CErrors.noncritical e -> (* Not eta-expanded or not reduced *)
     false
 
 let extract_nondep_branches test c b l =
@@ -631,7 +631,7 @@ and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl =
     let mat = build_tree Anonymous (snd flags) (avoid,env) ci bl in
     List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype flags avoid env sigma c))
       mat
-  with e when Errors.noncritical e ->
+  with e when CErrors.noncritical e ->
     Array.to_list
       (Array.map3 (detype_eqn flags avoid env sigma) constructs consnargsl bl)
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 729006dbb4..0fea2ba223 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,12 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Term
 open Vars
-open Closure
+open CClosure
 open Reduction
 open Reductionops
 open Termops
@@ -766,7 +766,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	       in Success evd'
 	     with Univ.UniverseInconsistency p ->
                UnifFailure (evd,UnifUnivInconsistency p)
-	     | e when Errors.noncritical e -> UnifFailure (evd,NotSameHead))
+	     | e when CErrors.noncritical e -> UnifFailure (evd,NotSameHead))
 
 	| Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty ->
             ise_and evd
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 77b0c67ad5..62700aef3c 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Util
-open Errors
+open CErrors
 open Names
 open Term
 open Vars
@@ -1460,7 +1460,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
                   map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
                     imitate envk t in
                 t::l
-              with e when Errors.noncritical e -> l in
+              with e when CErrors.noncritical e -> l in
             (match candidates with
             | [x] -> x
             | _ ->
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index df1fc20f1d..4caa1e9927 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -8,7 +8,7 @@
 
 open Pp
 open Util
-open Errors
+open CErrors
 open Names
 open Locus
 open Term
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 866b2b495d..0c80bd0193 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -11,7 +11,7 @@
 (* This file builds various inductive schemes *)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Libnames
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 6be6a2d3a2..fbad0d949d 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.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/pretyping/locusops.ml b/pretyping/locusops.ml
index d89aeccd8c..e4fbf8d542 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -50,9 +50,9 @@ let is_nowhere = function
 
 let simple_clause_of enum_hyps cl =
   let error_occurrences () =
-    Errors.error "This tactic does not support occurrences selection" in
+    CErrors.error "This tactic does not support occurrences selection" in
   let error_body_selection () =
-    Errors.error "This tactic does not support body selection" in
+    CErrors.error "This tactic does not support body selection" in
   let hyps =
     match cl.onhyps with
     | None ->
@@ -84,7 +84,7 @@ let concrete_clause_of enum_hyps cl =
 (** Miscellaneous functions *)
 
 let out_arg = function
-  | Misctypes.ArgVar _ -> Errors.anomaly (Pp.str "Unevaluated or_var variable")
+  | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable")
   | Misctypes.ArgArg x -> x
 
 let occurrences_of_hyp id cls =
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index e537a3c0ae..0dd64697c6 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 open Pp
-open Errors
+open CErrors
 open Term
 open Vars
 open Environ
@@ -178,7 +178,7 @@ let rec nf_val env v typ =
       let name,dom,codom = 
 	try decompose_prod env typ
 	with DestKO ->
-          Errors.anomaly
+          CErrors.anomaly
             (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
       in
       let env = push_rel (LocalAssum (name,dom)) env in
@@ -224,7 +224,7 @@ and nf_args env accu t =
     let _,dom,codom =
       try decompose_prod env t with
 	DestKO ->
-	Errors.anomaly
+	CErrors.anomaly
 	  (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
     in
     let c = nf_val env arg dom in
@@ -241,7 +241,7 @@ and nf_bargs env b t =
       let _,dom,codom =
 	try decompose_prod env !t with
 	  DestKO ->
-	  Errors.anomaly
+	  CErrors.anomaly
 	    (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
       in
       let c = nf_val env (block_field b i) dom in
@@ -352,7 +352,7 @@ and  nf_predicate env ind mip params v pT =
       let name,dom,codom =
 	try decompose_prod env pT with
 	  DestKO ->
-	  Errors.anomaly
+	  CErrors.anomaly
 	    (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
       in
       let dep,body = 
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 7eb3d633da..fe73b6105b 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Globnames
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index b0715af734..00b6100c02 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -60,7 +60,7 @@ type pretype_error =
 exception PretypeError of env * Evd.evar_map * pretype_error
 
 let precatchable_exception = function
-  | Errors.UserError _ | TypeError _ | PretypeError _
+  | CErrors.UserError _ | TypeError _ | PretypeError _
   | Nametab.GlobalizationError _ -> true
   | _ -> false
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 38defe9510..c8f61c66b8 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -22,7 +22,7 @@
 
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Evd
@@ -81,7 +81,7 @@ let search_guard loc env possible_indexes fixdefs =
     let fix = ((indexes, 0),fixdefs) in
     (try check_fix env fix
      with reraise ->
-       let (e, info) = Errors.push reraise in
+       let (e, info) = CErrors.push reraise in
        let info = Loc.add_loc info loc in
        iraise (e, info));
     indexes
@@ -228,8 +228,8 @@ let apply_heuristics env evdref fail_evar =
   (* Resolve eagerly, potentially making wrong choices *)
   try evdref := consider_remaining_unif_problems
 	~ts:(Typeclasses.classes_transparent_state ()) env !evdref
-  with e when Errors.noncritical e ->
-    let e = Errors.push e in if fail_evar then iraise e
+  with e when CErrors.noncritical e ->
+    let e = CErrors.push e in if fail_evar then iraise e
 
 let check_typeclasses_instances_are_solved env current_sigma frozen =
   (* Naive way, call resolution again with failure flag *)
@@ -624,7 +624,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
 	  let cofix = (i,(names,ftys,fdefs)) in
             (try check_cofix env cofix
              with reraise ->
-               let (e, info) = Errors.push reraise in
+               let (e, info) = CErrors.push reraise in
                let info = Loc.add_loc info loc in
                iraise (e, info));
 	    make_judge (mkCoFix cofix) ftys.(i)
@@ -757,7 +757,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
       try
         judge_of_product env name j j'
       with TypeError _ as e ->
-        let (e, info) = Errors.push e in
+        let (e, info) = CErrors.push e in
         let info = Loc.add_loc info loc in
         iraise (e, info) in
       inh_conv_coerce_to_tycon loc env evdref resj tycon
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 253d85742d..b4333847b7 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Term
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 95c6725f3c..682a883338 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -13,7 +13,7 @@
 (* This file registers properties of records: projections and
    canonical structures *)
 
-open Errors
+open CErrors
 open Util
 open Pp
 open Names
@@ -176,7 +176,7 @@ let cs_pattern_of_constr t =
       App (f,vargs) ->
 	begin
 	  try Const_cs (global_of_constr f) , None, Array.to_list vargs
-          with e when Errors.noncritical e -> raise Not_found
+          with e when CErrors.noncritical e -> raise Not_found
 	end
     | Rel n -> Default_cs, Some n, []
     | Prod (_,a,b) when not (Termops.dependent (mkRel 1) b) -> Prod_cs, None, [a; Termops.pop b]
@@ -184,7 +184,7 @@ let cs_pattern_of_constr t =
     | _ ->
 	begin
 	  try Const_cs (global_of_constr t) , None, []
-          with e when Errors.noncritical e -> raise Not_found
+          with e when CErrors.noncritical e -> raise Not_found
 	end
 
 let warn_projection_no_head_constant =
diff --git a/pretyping/redops.ml b/pretyping/redops.ml
index db5879174d..7d65925e57 100644
--- a/pretyping/redops.ml
+++ b/pretyping/redops.ml
@@ -20,12 +20,12 @@ let make_red_flag l =
     | FZeta :: lf -> add_flag { red with rZeta = true } lf
     | FConst l :: lf ->
 	if red.rDelta then
-	  Errors.error
+	  CErrors.error
 	    "Cannot set both constants to unfold and constants not to unfold";
         add_flag { red with rConst = union_consts red.rConst l } lf
     | FDeltaBut l :: lf ->
 	if red.rConst <> [] && not red.rDelta then
-	  Errors.error
+	  CErrors.error
 	    "Cannot set both constants to unfold and constants not to unfold";
         add_flag
           { red with rConst = union_consts red.rConst l; rDelta = true }
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 29b448caa3..5484e70b61 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Term
@@ -619,7 +619,7 @@ let rec strong_prodspine redfun sigma c =
 (*** Reduction using bindingss ***)
 (*************************************)
 
-let eta = Closure.RedFlags.mkflags [Closure.RedFlags.fETA]
+let eta = CClosure.RedFlags.mkflags [CClosure.RedFlags.fETA]
 
 (* Beta Reduction tools *)
 
@@ -798,11 +798,11 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
       (s,cst_l)
     in
     match kind_of_term x with
-    | Rel n when Closure.RedFlags.red_set flags Closure.RedFlags.fDELTA ->
+    | Rel n when CClosure.RedFlags.red_set flags CClosure.RedFlags.fDELTA ->
       (match lookup_rel n env with
       | LocalDef (_,body,_) -> whrec Cst_stack.empty (lift n body, stack)
       | _ -> fold ())
-    | Var id when Closure.RedFlags.red_set flags (Closure.RedFlags.fVAR id) ->
+    | Var id when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fVAR id) ->
       (match lookup_named id env with
       | LocalDef (_,body,_) -> whrec (Cst_stack.add_cst (mkVar id) cst_l) (body, stack)
       | _ -> fold ())
@@ -814,7 +814,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
       (match safe_meta_value sigma ev with
       | Some body -> whrec cst_l (body, stack)
       | None -> fold ())
-    | Const (c,u as const) when Closure.RedFlags.red_set flags (Closure.RedFlags.fCONST c) ->
+    | Const (c,u as const) when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) ->
        (match constant_opt_value_in env const with
 	| None -> fold ()
 	| Some body ->
@@ -854,7 +854,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
 		      whrec Cst_stack.empty 
 			(arg,Stack.Cst(Stack.Cst_const const,curr,remains,bef,cst_l)::s')
        )
-    | Proj (p, c) when Closure.RedFlags.red_projection flags p ->
+    | Proj (p, c) when CClosure.RedFlags.red_projection flags p ->
       (let pb = lookup_projection p env in
        let kn = Projection.constant p in
        let npars = pb.Declarations.proj_npars 
@@ -895,7 +895,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
 		       (arg,Stack.Cst(Stack.Cst_proj p,curr,remains,
 				      Stack.append_app [|c|] bef,cst_l)::s'))
 
-    | LetIn (_,b,_,c) when Closure.RedFlags.red_set flags Closure.RedFlags.fZETA ->
+    | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA ->
       apply_subst whrec [b] cst_l c stack
     | Cast (c,_,_) -> whrec cst_l (c, stack)
     | App (f,cl)  ->
@@ -904,9 +904,9 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
 	(f, Stack.append_app cl stack)
     | Lambda (na,t,c) ->
       (match Stack.decomp stack with
-      | Some _ when Closure.RedFlags.red_set flags Closure.RedFlags.fBETA ->
+      | Some _ when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA ->
 	apply_subst whrec [] cst_l x stack
-      | None when Closure.RedFlags.red_set flags Closure.RedFlags.fETA ->
+      | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA ->
 	let env' = push_rel (LocalAssum (na,t)) env in
 	let whrec' = whd_state_gen tactic_mode flags env' sigma in
         (match kind_of_term (Stack.zip ~refold:true (fst (whrec' (c, Stack.empty)))) with
@@ -934,8 +934,8 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
 	whrec Cst_stack.empty (arg, Stack.Fix(f,bef,cst_l)::s'))
 
     | Construct ((ind,c),u) ->
-      let use_match = Closure.RedFlags.red_set flags Closure.RedFlags.fMATCH in
-      let use_fix = Closure.RedFlags.red_set flags Closure.RedFlags.fFIX in
+      let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in
+      let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in
       if use_match || use_fix then
 	match Stack.strip_app stack with
 	|args, (Stack.Case(ci, _, lf,_)::s') when use_match ->
@@ -978,7 +978,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
       else fold ()
 
     | CoFix cofix ->
-      if Closure.RedFlags.red_set flags Closure.RedFlags.fCOFIX then
+      if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then
 	match Stack.strip_app stack with
 	|args, ((Stack.Case _ |Stack.Proj _)::s') ->
 	  reduce_and_refold_cofix whrec env cst_l cofix stack
@@ -996,15 +996,15 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
 let local_whd_state_gen flags sigma =
   let rec whrec (x, stack as s) =
     match kind_of_term x with
-    | LetIn (_,b,_,c) when Closure.RedFlags.red_set flags Closure.RedFlags.fZETA ->
+    | LetIn (_,b,_,c) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fZETA ->
       stacklam whrec [b] c stack
     | Cast (c,_,_) -> whrec (c, stack)
     | App (f,cl)  -> whrec (f, Stack.append_app cl stack)
     | Lambda (_,_,c) ->
       (match Stack.decomp stack with
-      | Some (a,m) when Closure.RedFlags.red_set flags Closure.RedFlags.fBETA ->
+      | Some (a,m) when CClosure.RedFlags.red_set flags CClosure.RedFlags.fBETA ->
 	stacklam whrec [a] c m
-      | None when Closure.RedFlags.red_set flags Closure.RedFlags.fETA ->
+      | None when CClosure.RedFlags.red_set flags CClosure.RedFlags.fETA ->
         (match kind_of_term (Stack.zip (whrec (c, Stack.empty))) with
         | App (f,cl) ->
 	  let napp = Array.length cl in
@@ -1020,7 +1020,7 @@ let local_whd_state_gen flags sigma =
 	| _ -> s)
       | _ -> s)
 
-    | Proj (p,c) when Closure.RedFlags.red_projection flags p ->
+    | Proj (p,c) when CClosure.RedFlags.red_projection flags p ->
       (let pb = lookup_projection p (Global.env ()) in
 	 whrec (c, Stack.Proj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, 
 			       p, Cst_stack.empty)
@@ -1045,8 +1045,8 @@ let local_whd_state_gen flags sigma =
       | None -> s)
 
     | Construct ((ind,c),u) ->
-      let use_match = Closure.RedFlags.red_set flags Closure.RedFlags.fMATCH in
-      let use_fix = Closure.RedFlags.red_set flags Closure.RedFlags.fFIX in
+      let use_match = CClosure.RedFlags.red_set flags CClosure.RedFlags.fMATCH in
+      let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in
       if use_match || use_fix then
 	match Stack.strip_app stack with
 	|args, (Stack.Case(ci, _, lf,_)::s') when use_match ->
@@ -1061,7 +1061,7 @@ let local_whd_state_gen flags sigma =
       else s
 
     | CoFix cofix ->
-      if Closure.RedFlags.red_set flags Closure.RedFlags.fCOFIX then
+      if CClosure.RedFlags.red_set flags CClosure.RedFlags.fCOFIX then
 	match Stack.strip_app stack with
 	|args, ((Stack.Case _ | Stack.Proj _)::s') ->
 	  whrec (contract_cofix cofix, stack)
@@ -1093,27 +1093,27 @@ let red_of_state_red f sigma x =
 
 (* 0. No Reduction Functions *)
 
-let whd_nored_state = local_whd_state_gen Closure.nored
+let whd_nored_state = local_whd_state_gen CClosure.nored
 let whd_nored_stack = stack_red_of_state_red whd_nored_state
 let whd_nored = red_of_state_red whd_nored_state
 
 (* 1. Beta Reduction Functions *)
 
-let whd_beta_state = local_whd_state_gen Closure.beta
+let whd_beta_state = local_whd_state_gen CClosure.beta
 let whd_beta_stack = stack_red_of_state_red whd_beta_state
 let whd_beta = red_of_state_red whd_beta_state
 
-let whd_betalet_state = local_whd_state_gen Closure.betazeta
+let whd_betalet_state = local_whd_state_gen CClosure.betazeta
 let whd_betalet_stack = stack_red_of_state_red whd_betalet_state
 let whd_betalet = red_of_state_red whd_betalet_state
 
 (* 2. Delta Reduction Functions *)
 
-let whd_delta_state e = raw_whd_state_gen Closure.delta e
+let whd_delta_state e = raw_whd_state_gen CClosure.delta e
 let whd_delta_stack env = stack_red_of_state_red (whd_delta_state env)
 let whd_delta env = red_of_state_red  (whd_delta_state env)
 
-let whd_betadeltazeta_state e = raw_whd_state_gen Closure.betadeltazeta e
+let whd_betadeltazeta_state e = raw_whd_state_gen CClosure.betadeltazeta e
 let whd_betadeltazeta_stack env =
   stack_red_of_state_red (whd_betadeltazeta_state env)
 let whd_betadeltazeta env =
@@ -1122,21 +1122,21 @@ let whd_betadeltazeta env =
 
 (* 3. Iota reduction Functions *)
 
-let whd_betaiota_state = local_whd_state_gen Closure.betaiota
+let whd_betaiota_state = local_whd_state_gen CClosure.betaiota
 let whd_betaiota_stack = stack_red_of_state_red whd_betaiota_state
 let whd_betaiota = red_of_state_red whd_betaiota_state
 
-let whd_betaiotazeta_state = local_whd_state_gen Closure.betaiotazeta
+let whd_betaiotazeta_state = local_whd_state_gen CClosure.betaiotazeta
 let whd_betaiotazeta_stack = stack_red_of_state_red whd_betaiotazeta_state
 let whd_betaiotazeta = red_of_state_red whd_betaiotazeta_state
 
-let whd_all_state env = raw_whd_state_gen Closure.all env
+let whd_all_state env = raw_whd_state_gen CClosure.all env
 let whd_all_stack env =
   stack_red_of_state_red (whd_all_state env)
 let whd_all env =
   red_of_state_red (whd_all_state env)
 
-let whd_allnolet_state env = raw_whd_state_gen Closure.allnolet env
+let whd_allnolet_state env = raw_whd_state_gen CClosure.allnolet env
 let whd_allnolet_stack env =
   stack_red_of_state_red (whd_allnolet_state env)
 let whd_allnolet env =
@@ -1148,7 +1148,7 @@ let shrink_eta c = Stack.zip (local_whd_state_gen eta Evd.empty (c,Stack.empty))
 
 (* 5. Zeta Reduction Functions *)
 
-let whd_zeta_state = local_whd_state_gen Closure.zeta
+let whd_zeta_state = local_whd_state_gen CClosure.zeta
 let whd_zeta_stack = stack_red_of_state_red whd_zeta_state
 let whd_zeta = red_of_state_red whd_zeta_state
 
@@ -1166,16 +1166,16 @@ let nf_evar = Evarutil.nf_evar
 let clos_norm_flags flgs env sigma t =
   try
     let evars ev = safe_evar_value sigma ev in
-    Closure.norm_val
-      (Closure.create_clos_infos ~evars flgs env)
-      (Closure.inject t)
+    CClosure.norm_val
+      (CClosure.create_clos_infos ~evars flgs env)
+      (CClosure.inject t)
   with e when is_anomaly e -> error "Tried to normalize ill-typed term"
 
-let nf_beta = clos_norm_flags Closure.beta (Global.env ())
-let nf_betaiota = clos_norm_flags Closure.betaiota (Global.env ())
-let nf_betaiotazeta = clos_norm_flags Closure.betaiotazeta (Global.env ())
+let nf_beta = clos_norm_flags CClosure.beta (Global.env ())
+let nf_betaiota = clos_norm_flags CClosure.betaiota (Global.env ())
+let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta (Global.env ())
 let nf_all env sigma =
-  clos_norm_flags Closure.all env sigma
+  clos_norm_flags CClosure.all env sigma
 
 
 (********************************************************************)
@@ -1206,7 +1206,7 @@ let pb_equal = function
 
 let report_anomaly _ =
   let e = UserError ("", Pp.str "Conversion test raised an anomaly") in
-  let e = Errors.push e in
+  let e = CErrors.push e in
   iraise e
 
 let test_trans_conversion (f: constr Reduction.extended_conversion_function) reds env sigma x y =
@@ -1469,19 +1469,19 @@ let is_sort env sigma t =
 
 let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
   let rec whrec csts s =
-    let (t, stack as s),csts' = whd_state_gen ~csts false Closure.betaiota env sigma s in
+    let (t, stack as s),csts' = whd_state_gen ~csts false CClosure.betaiota env sigma s in
     match Stack.strip_app stack with
       |args, (Stack.Case _ :: _ as stack') ->
 	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
-	  (Closure.RedFlags.red_add_transparent Closure.all ts) env sigma (t,args) in
+	  (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
 	if reducible_mind_case t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
       |args, (Stack.Fix _ :: _ as stack') ->
 	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
-	  (Closure.RedFlags.red_add_transparent Closure.all ts) env sigma (t,args) in
+	  (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
 	if isConstruct t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
       |args, (Stack.Proj (n,m,p,_) :: stack'') ->
 	let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
-	  (Closure.RedFlags.red_add_transparent Closure.all ts) env sigma (t,args) in
+	  (CClosure.RedFlags.red_add_transparent CClosure.all ts) env sigma (t,args) in
 	if isConstruct t_o then
 	  whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'')
 	else s,csts'
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index fdfa77412e..874ea6815e 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -134,15 +134,15 @@ val stack_reduction_of_reduction :
 i*)
 val stacklam : (state -> 'a) -> constr list -> constr -> constr Stack.t -> 'a
 
-val whd_state_gen : ?csts:Cst_stack.t -> bool -> Closure.RedFlags.reds ->
+val whd_state_gen : ?csts:Cst_stack.t -> bool -> CClosure.RedFlags.reds ->
   Environ.env -> Evd.evar_map -> state -> state * Cst_stack.t
 
-val iterate_whd_gen : bool -> Closure.RedFlags.reds ->
+val iterate_whd_gen : bool -> CClosure.RedFlags.reds ->
   Environ.env -> Evd.evar_map -> Term.constr -> Term.constr
 
 (** {6 Generic Optimized Reduction Function using Closures } *)
 
-val clos_norm_flags : Closure.RedFlags.reds -> reduction_function
+val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function
 
 (** Same as [(strong whd_beta[delta][iota])], but much faster on big terms *)
 val nf_beta : local_reduction_function
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 5de540a000..98b36fb92f 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Term
 open Vars
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 51a89966fe..820a81b5d2 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Term
@@ -18,7 +18,7 @@ open Termops
 open Find_subterm
 open Namegen
 open Environ
-open Closure
+open CClosure
 open Reductionops
 open Cbv
 open Patternops
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 195b21bbf2..f8dfe1adf2 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -66,7 +66,7 @@ val pattern_occs : (occurrences * constr) list -> e_reduction_function
 (** Rem: Lazy strategies are defined in Reduction *)
 
 (** Call by value strategy (uses Closures) *)
-val cbv_norm_flags : Closure.RedFlags.reds ->  reduction_function
+val cbv_norm_flags : CClosure.RedFlags.reds ->  reduction_function
   val cbv_beta : local_reduction_function
   val cbv_betaiota : local_reduction_function
   val cbv_betadeltaiota :  reduction_function
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d57eef2e1f..2c675b9eae 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -150,7 +150,7 @@ let dest_class_arity env c =
 
 let class_of_constr c =
   try Some (dest_class_arity (Global.env ()) c)
-  with e when Errors.noncritical e -> None
+  with e when CErrors.noncritical e -> None
 
 let is_class_constr c = 
   try let gr, u = Universes.global_of_constr c in
@@ -249,7 +249,7 @@ let rebuild_class cl =
   try 
     let cst = Tacred.evaluable_of_global_reference (Global.env ()) cl.cl_impl in
       set_typeclass_transparency cst false false; cl
-  with e when Errors.noncritical e -> cl
+  with e when CErrors.noncritical e -> cl
 
 let class_input : typeclass -> obj =
   declare_object
@@ -272,7 +272,7 @@ let check_instance env sigma c =
     let (evd, c) = resolve_one_typeclass env sigma
       (Retyping.get_type_of env sigma c) in
       not (Evd.has_undefined evd)
-  with e when Errors.noncritical e -> false
+  with e when CErrors.noncritical e -> false
 
 let build_subclasses ~check env sigma glob pri =
   let _id = Nametab.basename_of_global glob in
@@ -422,7 +422,7 @@ let add_class cl =
 	     match inst with
 	     | Some (Backward, pri) ->
 	       (match body with
-	       | None -> Errors.error "Non-definable projection can not be declared as a subinstance"
+	       | None -> CErrors.error "Non-definable projection can not be declared as a subinstance"
 	       | Some b -> declare_instance pri false (ConstRef b))
 	     | _ -> ())
   cl.cl_projs
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 8e44fb0082..0e4885bead 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Term
 open Vars
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5bb853b694..0c1ce0d2f8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Pp
 open Util
 open Names
@@ -460,7 +460,7 @@ let use_metas_pattern_unification flags nb l =
      Array.for_all (fun c -> isRel c && destRel c <= nb) l
 
 type key = 
-  | IsKey of Closure.table_key
+  | IsKey of CClosure.table_key
   | IsProj of projection * constr
 
 let expand_table_key env = function
@@ -742,7 +742,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 		 then Evd.set_leq_sort curenv sigma s1 s2 
 		 else Evd.set_eq_sort curenv sigma s1 s2
 	       in (sigma', metasubst, evarsubst)
-	     with e when Errors.noncritical e ->
+	     with e when CErrors.noncritical e ->
                error_cannot_unify curenv sigma (m,n))
 
 	| Lambda (na,t1,c1), Lambda (_,t2,c2) ->
@@ -1138,11 +1138,11 @@ let merge_instances env sigma flags st1 st2 c1 c2 =
       else (right, st2, res)
   | (IsSuperType,IsSubType) ->
     (try (left, IsSubType, unify_0 env sigma CUMUL flags c2 c1)
-     with e when Errors.noncritical e ->
+     with e when CErrors.noncritical e ->
        (right, IsSubType, unify_0 env sigma CUMUL flags c1 c2))
   | (IsSubType,IsSuperType) ->
     (try (left, IsSuperType, unify_0 env sigma CUMUL flags c1 c2)
-     with e when Errors.noncritical e ->
+     with e when CErrors.noncritical e ->
        (right, IsSuperType, unify_0 env sigma CUMUL flags c2 c1))
     
 (* Unification
@@ -1210,8 +1210,8 @@ let applyHead env (type r) (evd : r Sigma.t) n c =
 
 let is_mimick_head ts f =
   match kind_of_term f with
-  | Const (c,u) -> not (Closure.is_transparent_constant ts c)
-  | Var id -> not (Closure.is_transparent_variable ts id)
+  | Const (c,u) -> not (CClosure.is_transparent_constant ts c)
+  | Var id -> not (CClosure.is_transparent_variable ts id)
   | (Rel _|Construct _|Ind _) -> true
   | _ -> false
 
@@ -1353,7 +1353,7 @@ let w_merge env with_types flags (evd,metas,evars) =
 	let rec process_eqns failures = function
 	  | (mv,status,c)::eqns ->
               (match (try Inl (unify_type env evd flags mv status c)
-		      with e when Errors.noncritical e -> Inr e)
+		      with e when CErrors.noncritical e -> Inr e)
 	       with 
 	       | Inr e -> process_eqns (((mv,status,c),e)::failures) eqns
 	       | Inl (evd,metas,evars) ->
@@ -1555,7 +1555,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
     | PretypeError (_,_,CannotUnify (c1,c2,Some e)) ->
         raise (NotUnifiable (Some (c1,c2,e)))
     (** MS: This is pretty bad, it catches Not_found for example *)
-    | e when Errors.noncritical e -> raise (NotUnifiable None) in
+    | e when CErrors.noncritical e -> raise (NotUnifiable None) in
   let merge_fun c1 c2 =
     match c1, c2 with
     | Some (evd,c1,x), Some (_,c2,_) ->
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 0b102f9218..c396f593bb 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -305,7 +305,7 @@ and nf_fun env f typ =
     try decompose_prod env typ
     with DestKO ->
       (* 27/2/13: Turned this into an anomaly *)
-      Errors.anomaly
+      CErrors.anomaly
         (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
   in
   let body = nf_val (push_rel (LocalAssum (name,dom)) env) vb codom in