closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)

 For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a

30 files changed, 121 insertions, 122 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 9b4998c67..a2a7437fb 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -86,7 +86,7 @@ Nativecode
 Nativelib
 Cbytegen
 Environ
-Closure
+CClosure
 Reduction
 Nativeconv
 Type_errors
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 7c010e6a4..023835af7 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -80,7 +80,7 @@ let ppconstr_univ x = Constrextern.with_universes ppconstr x
 let ppglob_constr = (fun x -> pp(pr_lglob_constr x))
 let pppattern = (fun x -> pp(pr_constr_pattern x))
 let pptype = (fun x -> try pp(pr_ltype x) with e -> pp (str (Printexc.to_string e)))
-let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
+let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
 
 let ppbigint n = pp (str (Bigint.to_string n));;
 
@@ -457,7 +457,7 @@ let print_pure_constr csr =
 	print_string (Printexc.to_string e);print_flush ();
 	raise e
 
-let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
+let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
 
 let pploc x = let (l,r) = Loc.unloc x in
   print_string"(";print_int l;print_string",";print_int r;print_string")"
diff --git a/kernel/closure.ml b/kernel/cClosure.ml
index 04c1bb657..d475f097c 100644
--- a/kernel/closure.ml
+++ b/kernel/cClosure.ml
@@ -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 76145e3f8..077756ac7 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/kernel.mllib b/kernel/kernel.mllib
index 1e132e3ab..15f213ce9 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/reduction.ml b/kernel/reduction.ml
index 67b05e526..6c664f791 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -21,7 +21,7 @@ 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/ltac/rewrite.ml b/ltac/rewrite.ml
index e0ae98ffa..0556191be 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1466,7 +1466,7 @@ let solve_constraints env (evars,cstrs) =
       (Typeclasses.mark_resolvables ~filter evars)
       
 let nf_zeta =
-  Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+  Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
 
 exception RewriteFailure of Pp.std_ppcmds
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 6f6122d50..aff60eaa4 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -38,12 +38,12 @@ let _True = reference ["Init";"Logic"] "True"
 let _I = reference ["Init";"Logic"] "I"
 
 let whd env=
-  let infos=Closure.create_clos_infos Closure.betaiotazeta env in
-    (fun t -> Closure.whd_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos CClosure.betaiotazeta env in
+    (fun t -> CClosure.whd_val infos (CClosure.inject t))
 
 let whd_delta env=
-   let infos=Closure.create_clos_infos Closure.all env in
-    (fun t -> Closure.whd_val infos (Closure.inject t))
+   let infos=CClosure.create_clos_infos CClosure.all env in
+    (fun t -> CClosure.whd_val infos (CClosure.inject t))
 
 (* decompose member of equality in an applicative format *)
 
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 10c09c8d6..a862423e9 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -153,8 +153,8 @@ let interp_constr check_sort env sigma c =
     fst (understand env sigma (fst c))
 
 let special_whd env =
-  let infos=Closure.create_clos_infos Closure.all env in
-    (fun t -> Closure.whd_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos CClosure.all env in
+    (fun t -> CClosure.whd_val infos (CClosure.inject t))
 
 let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq))
 
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 5ed426c1d..97c9d5f4a 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -84,12 +84,12 @@ let tcl_erase_info gls =
   tcl_change_info_gen info_gen gls
 
 let special_whd gl=
-  let infos=Closure.create_clos_infos Closure.all (pf_env gl) in
-    (fun t -> Closure.whd_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in
+    (fun t -> CClosure.whd_val infos (CClosure.inject t))
 
 let special_nf gl=
-  let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in
-    (fun t -> Closure.norm_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in
+    (fun t -> CClosure.norm_val infos (CClosure.inject t))
 
 let is_good_inductive env ind =
   let mib,oib = Inductive.lookup_mind_specif env ind in
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 2ed436c6b..58744b575 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -19,7 +19,7 @@ open Context.Rel.Declaration
 
 let qflag=ref true
 
-let red_flags=ref Closure.betaiotazeta
+let red_flags=ref CClosure.betaiotazeta
 
 let (=?) f g i1 i2 j1 j2=
   let c=f i1 i2 in
@@ -59,12 +59,12 @@ let ind_hyps nevar ind largs gls=
     Array.map myhyps types
 
 let special_nf gl=
-  let infos=Closure.create_clos_infos !red_flags (pf_env gl) in
-    (fun t -> Closure.norm_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in
+    (fun t -> CClosure.norm_val infos (CClosure.inject t))
 
 let special_whd gl=
-  let infos=Closure.create_clos_infos !red_flags (pf_env gl) in
-    (fun t -> Closure.whd_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in
+    (fun t -> CClosure.whd_val infos (CClosure.inject t))
 
 type kind_of_formula=
     Arrow of constr*constr
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 0f70d3ea0..5db8ff59a 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -11,7 +11,7 @@ open Globnames
 
 val qflag : bool ref
 
-val red_flags: Closure.RedFlags.reds ref
+val red_flags: CClosure.RedFlags.reds ref
 
 val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) ->
   'a -> 'a -> 'b -> 'b -> int
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index d7da85b4f..628af4e71 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -24,8 +24,8 @@ let update_flags ()=
   in
     List.iter f (Classops.coercions ());
     red_flags:=
-    Closure.RedFlags.red_add_transparent
-      Closure.betaiotazeta
+    CClosure.RedFlags.red_add_transparent
+      CClosure.betaiotazeta
       (Names.Id.Pred.full,Names.Cpred.complement !predref)
 
 let ground_tac solver startseq gl=
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 13bc81019..215c850b6 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -223,8 +223,8 @@ let isAppConstruct ?(env=Global.env ()) t =
 
 let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta  *)
   let clos_norm_flags flgs env sigma t =
-    Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
-  clos_norm_flags Closure.betaiotazeta  Environ.empty_env Evd.empty
+    CClosure.norm_val (CClosure.create_clos_infos flgs env) (CClosure.inject (Reductionops.nf_evar sigma t)) in
+  clos_norm_flags CClosure.betaiotazeta  Environ.empty_env Evd.empty
 
 
 
@@ -1085,7 +1085,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
       match Global.body_of_constant const with
 	| Some body ->
 	     Tacred.cbv_norm_flags
-	       (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+	       (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
 	       (Global.env ())
 	       (Evd.empty)
 	       body
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 18ef53276..5e72b8672 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -400,7 +400,7 @@ let get_funs_constant mp dp =
       match Global.body_of_constant const with
 	| Some body ->
 	    let body = Tacred.cbv_norm_flags
-	      (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+	      (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
 	      (Global.env ())
 	      (Evd.from_env (Global.env ()))
 	      body
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index ad5d077d6..e0c60d6d5 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -90,7 +90,7 @@ let observe_tac s tac g =
 
 (* [nf_zeta] $\zeta$-normalization of a term *)
 let nf_zeta =
-  Reductionops.clos_norm_flags  (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+  Reductionops.clos_norm_flags  (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
     Environ.empty_env
     Evd.empty
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5562100e9..027fe5677 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -92,15 +92,15 @@ let const_of_ref = function
 
 
 let nf_zeta env =
-  Reductionops.clos_norm_flags  (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+  Reductionops.clos_norm_flags  (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
     env
     Evd.empty
 
 
 let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta  *)
   let clos_norm_flags flgs env sigma t =
-    Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
-  clos_norm_flags Closure.betaiotazeta  Environ.empty_env Evd.empty
+    CClosure.norm_val (CClosure.create_clos_infos flgs env) (CClosure.inject (Reductionops.nf_evar sigma t)) in
+  clos_norm_flags CClosure.betaiotazeta  Environ.empty_env Evd.empty
 
 
 
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 7367a47ea..4ed907951 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -67,12 +67,12 @@ let l_D_Or = lazy (constant "D_Or")
 
 
 let special_whd gl=
-  let infos=Closure.create_clos_infos Closure.all (pf_env gl) in
-    (fun t -> Closure.whd_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in
+    (fun t -> CClosure.whd_val infos (CClosure.inject t))
 
 let special_nf gl=
-  let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in
-    (fun t -> Closure.norm_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in
+    (fun t -> CClosure.norm_val infos (CClosure.inject t))
 
 type atom_env=
     {mutable next:int;
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index c08813f6e..90f5f8e63 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -12,7 +12,7 @@ open Util
 open Names
 open Term
 open Vars
-open Closure
+open CClosure
 open Environ
 open Libnames
 open Globnames
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 132147487..84bf849e7 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 de37d1fc5..87a03abbd 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/evarconv.ml b/pretyping/evarconv.ml
index 8abe6116b..0fea2ba22 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -11,7 +11,7 @@ open Util
 open Names
 open Term
 open Vars
-open Closure
+open CClosure
 open Reduction
 open Reductionops
 open Termops
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 76c4304c4..5484e70b6 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -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
 
 
 (********************************************************************)
@@ -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 fdfa77412..874ea6815 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/tacred.ml b/pretyping/tacred.ml
index 2d07bf4d5..820a81b5d 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -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 195b21bbf..f8dfe1adf 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/unification.ml b/pretyping/unification.ml
index c17879739..0c1ce0d2f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -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
@@ -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
 
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index ba883b5b2..8a9ce4f94 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -17,7 +17,7 @@ open Genredexpr
 open Pattern
 open Reductionops
 open Tacred
-open Closure
+open CClosure
 open RedFlags
 open Libobject
 open Misctypes
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 750f7a60c..1be5226de 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -262,7 +262,7 @@ let pperror cmd = CErrors.errorlabstrm "Program" cmd
 let error s = pperror (str s)
 
 let reduce c =
-  Reductionops.clos_norm_flags Closure.betaiota (Global.env ()) Evd.empty c
+  Reductionops.clos_norm_flags CClosure.betaiota (Global.env ()) Evd.empty c
 
 exception NoObligations of Id.t option
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 04c01f3cd..e4a2ca5a0 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1287,8 +1287,8 @@ let _ =
       optdepr  = false;
       optname  = "kernel term sharing";
       optkey   = ["Kernel"; "Term"; "Sharing"];
-      optread  = (fun () -> !Closure.share);
-      optwrite = (fun b -> Closure.share := b) }
+      optread  = (fun () -> !CClosure.share);
+      optwrite = (fun b -> CClosure.share := b) }
 
 (* No more undo limit in the new proof engine.
    The command still exists for compatibility (e.g. with ProofGeneral) *)