1 files changed, 28 insertions, 33 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 31ded9129a..219ea5b24a 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -91,6 +91,7 @@ module type RedFlagsSig = sig
   val red_add : reds -> red_kind -> reds
   val red_sub : reds -> red_kind -> reds
   val red_add_transparent : reds -> transparent_state -> reds
+  val red_transparent : reds -> transparent_state
   val mkflags : red_kind list -> reds
   val red_set : reds -> red_kind -> bool
   val red_projection : reds -> projection -> bool
@@ -164,6 +165,8 @@ module RedFlags = (struct
 	let (l1,l2) = red.r_const in
 	{ red with r_const = Id.Pred.remove id l1, l2 }
 
+  let red_transparent red = red.r_const
+
   let red_add_transparent red tr =
     { red with r_const = tr }
 
@@ -258,7 +261,7 @@ type 'a infos_cache = {
   i_repr : 'a infos -> constr -> 'a;
   i_env : env;
   i_sigma : existential -> constr option;
-  i_rels : constr option array;
+  i_rels : (Context.Rel.Declaration.t * Pre_env.lazy_val) Range.t;
   i_tab : 'a KeyTable.t }
 
 and 'a infos = {
@@ -282,13 +285,16 @@ let ref_value_cache ({i_cache = cache} as infos)  ref =
     let body =
       match ref with
 	| RelKey n ->
-            let len = Array.length cache.i_rels in
-            let i = n - 1 in
-            let () = if i < 0 || len <= i then raise Not_found in
-            begin match Array.unsafe_get cache.i_rels i with
-            | None -> raise Not_found
-            | Some t -> lift n t
-            end
+          let open Context.Rel.Declaration in
+          let i = n - 1 in
+          let (d, _) =
+            try Range.get cache.i_rels i
+            with Invalid_argument _ -> raise Not_found
+          in
+          begin match d with
+          | LocalAssum _ -> raise Not_found
+          | LocalDef (_, t, _) -> lift n t
+          end
 	| VarKey id -> assoc_defined id cache.i_env
 	| ConstKey cst -> constant_value_in cache.i_env cst
     in
@@ -303,26 +309,13 @@ let ref_value_cache ({i_cache = cache} as infos)  ref =
 let evar_value cache ev =
   cache.i_sigma ev
 
-let defined_rels flags env =
-(*  if red_local_const (snd flags) then*)
-  let ctx = rel_context env in
-  let len = List.length ctx in
-  let ans = Array.make len None in
-  let open Context.Rel.Declaration in
-  let iter i = function
-    | LocalAssum _ -> ()
-    | LocalDef (_,b,_) -> Array.unsafe_set ans i (Some b)
-  in
-  let () = List.iteri iter ctx in
-  ans
-(*  else (0,[])*)
-
 let create mk_cl flgs env evars =
+  let open Pre_env in
   let cache =
     { i_repr = mk_cl;
       i_env = env;
       i_sigma = evars;
-      i_rels = defined_rels flgs env;
+      i_rels = (Environ.pre_env env).env_rel_context.env_rel_map;
       i_tab = KeyTable.create 17 }
   in { i_flags = flgs; i_cache = cache }
 
@@ -810,7 +803,7 @@ 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 == Declarations.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
@@ -857,6 +850,14 @@ let contract_fix_vect fix =
   in
   (subs_cons(Array.init nfix make_body, env), thisbody)
 
+let unfold_projection info p =
+  if red_projection info.i_flags p
+  then
+    let open Declarations in
+    let pb = lookup_projection p (info_env info) in
+    Some (Zproj (pb.proj_npars, pb.proj_arg, Projection.constant p))
+  else None
+
 (*********************************************************************)
 (* A machine that inspects the head of a term until it finds an
    atom or a subterm that may produce a redex (abstraction,
@@ -875,15 +876,9 @@ let rec knh info m stk =
            | (None, stk') -> (m,stk'))
     | FCast(t,_,_) -> knh info t stk
     | FProj (p,c) ->
-      let unf = Projection.unfolded p in
-        if unf || red_set info.i_flags (fCONST (Projection.constant p)) then
-          (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,
-				Projection.constant p)
-			 :: zupdate m stk))
-	else (m,stk)
+      (match unfold_projection info p with
+       | None -> (m, stk)
+       | Some s -> knh info c (s :: zupdate m stk))
 
 (* cases where knh stops *)
     | (FFlex _|FLetIn _|FConstruct _|FEvar _|