Merge PR #6769: Split closure cache and remove whd_both

7 files changed, 131 insertions, 150 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 11faef02c..5f683790c 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -259,12 +259,14 @@ module KeyTable = Hashtbl.Make(IdKeyHash)
 
 let eq_table_key = IdKeyHash.equal
 
+type 'a infos_tab = 'a KeyTable.t
+
 type 'a infos_cache = {
-  i_repr : 'a infos -> constr -> 'a;
+  i_repr : 'a infos -> 'a infos_tab -> constr -> 'a;
   i_env : env;
   i_sigma : existential -> constr option;
   i_rels : (Context.Rel.Declaration.t * Pre_env.lazy_val) Range.t;
-  i_tab : 'a KeyTable.t }
+}
 
 and 'a infos = {
   i_flags : reds;
@@ -279,9 +281,9 @@ let assoc_defined id env = match Environ.lookup_named id env with
 | LocalDef (_, c, _) -> c
 | _ -> raise Not_found
 
-let ref_value_cache ({i_cache = cache} as infos)  ref =
+let ref_value_cache ({i_cache = cache} as infos) tab ref =
   try
-    Some (KeyTable.find cache.i_tab ref)
+    Some (KeyTable.find tab ref)
   with Not_found ->
   try
     let body =
@@ -300,8 +302,8 @@ let ref_value_cache ({i_cache = cache} as infos)  ref =
 	| VarKey id -> assoc_defined id cache.i_env
 	| ConstKey cst -> constant_value_in cache.i_env cst
     in
-    let v = cache.i_repr infos body in
-    KeyTable.add cache.i_tab ref v;
+    let v = cache.i_repr infos tab body in
+    KeyTable.add tab ref v;
     Some v
   with
     | Not_found (* List.assoc *)
@@ -318,7 +320,7 @@ let create mk_cl flgs env evars =
       i_env = env;
       i_sigma = evars;
       i_rels = (Environ.pre_env env).env_rel_context.env_rel_map;
-      i_tab = KeyTable.create 17 }
+    }
   in { i_flags = flgs; i_cache = cache }
 
 
@@ -906,23 +908,23 @@ and knht info e t stk =
 (************************************************************************)
 
 (* Computes a weak head normal form from the result of knh. *)
-let rec knr info m stk =
+let rec knr info tab m stk =
   match m.term with
   | FLambda(n,tys,f,e) when red_set info.i_flags fBETA ->
       (match get_args n tys f e stk with
-          Inl e', s -> knit info e' f s
+          Inl e', s -> knit info tab e' f s
         | Inr lam, s -> (lam,s))
   | FFlex(ConstKey (kn,_ as c)) when red_set info.i_flags (fCONST kn) ->
-      (match ref_value_cache info (ConstKey c) with
-          Some v -> kni info v stk
+      (match ref_value_cache info tab (ConstKey c) with
+          Some v -> kni info tab v stk
         | None -> (set_norm m; (m,stk)))
   | FFlex(VarKey id) when red_set info.i_flags (fVAR id) ->
-      (match ref_value_cache info (VarKey id) with
-          Some v -> kni info v stk
+      (match ref_value_cache info tab (VarKey id) with
+          Some v -> kni info tab v stk
         | None -> (set_norm m; (m,stk)))
   | FFlex(RelKey k) when red_set info.i_flags fDELTA ->
-      (match ref_value_cache info (RelKey k) with
-          Some v -> kni info v stk
+      (match ref_value_cache info tab (RelKey k) with
+          Some v -> kni info tab v stk
         | None -> (set_norm m; (m,stk)))
   | FConstruct((ind,c),u) ->
      let use_match = red_set info.i_flags fMATCH in
@@ -932,29 +934,29 @@ let rec knr info m stk =
         | (depth, args, ZcaseT(ci,_,br,e)::s) when use_match ->
             assert (ci.ci_npar>=0);
             let rargs = drop_parameters depth ci.ci_npar args in
-            knit info e br.(c-1) (rargs@s)
+            knit info tab e br.(c-1) (rargs@s)
         | (_, cargs, Zfix(fx,par)::s) when use_fix ->
             let rarg = fapp_stack(m,cargs) in
             let stk' = par @ append_stack [|rarg|] s in
             let (fxe,fxbd) = contract_fix_vect fx.term in
-            knit info fxe fxbd stk'
+            knit info tab fxe fxbd stk'
 	| (depth, args, Zproj (n, m, cst)::s) when use_match ->
 	    let rargs = drop_parameters depth n args in
 	    let rarg = project_nth_arg m rargs in
-	      kni info rarg s
+            kni info tab rarg s
         | (_,args,s) -> (m,args@s))
      else (m,stk)
   | FCoFix _ when red_set info.i_flags fCOFIX ->
       (match strip_update_shift_app m stk with
           (_, args, (((ZcaseT _|Zproj _)::_) as stk')) ->
             let (fxe,fxbd) = contract_fix_vect m.term in
-            knit info fxe fxbd (args@stk')
+            knit info tab fxe fxbd (args@stk')
         | (_,args,s) -> (m,args@s))
   | FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA ->
-      knit info (subs_cons([|v|],e)) bd stk
+      knit info tab (subs_cons([|v|],e)) bd stk
   | FEvar(ev,env) ->
       (match evar_value info.i_cache ev with
-          Some c -> knit info env c stk
+          Some c -> knit info tab env c stk
         | None -> (m,stk))
   | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FApp _ | FProj _
     | FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _
@@ -962,14 +964,14 @@ let rec knr info m stk =
 
 
 (* Computes the weak head normal form of a term *)
-and kni info m stk =
+and kni info tab m stk =
   let (hm,s) = knh info m stk in
-  knr info hm s
-and knit info e t stk =
+  knr info tab hm s
+and knit info tab e t stk =
   let (ht,s) = knht info e t stk in
-  knr info ht s
+  knr info tab ht s
 
-let kh info v stk = fapp_stack(kni info v stk)
+let kh info tab v stk = fapp_stack(kni info tab v stk)
 
 (************************************************************************)
 
@@ -997,61 +999,61 @@ let rec zip_term zfun m stk =
    1- Calls kni
    2- tries to rebuild the term. If a closure still has to be computed,
       calls itself recursively. *)
-let rec kl info m =
+let rec kl info tab m =
   if is_val m then (incr prune; term_of_fconstr m)
   else
-    let (nm,s) = kni info m [] in
+    let (nm,s) = kni info tab m [] in
     let () = if !share then ignore (fapp_stack (nm, s)) in (* to unlock Zupdates! *)
-    zip_term (kl info) (norm_head info nm) s
+    zip_term (kl info tab) (norm_head info tab nm) s
 
 (* no redex: go up for atoms and already normalized terms, go down
    otherwise. *)
-and norm_head info m =
+and norm_head info tab m =
   if is_val m then (incr prune; term_of_fconstr m) else
     match m.term with
       | FLambda(n,tys,f,e) ->
           let (e',rvtys) =
             List.fold_left (fun (e,ctxt) (na,ty) ->
-              (subs_lift e, (na,kl info (mk_clos e ty))::ctxt))
+              (subs_lift e, (na,kl info tab (mk_clos e ty))::ctxt))
               (e,[]) tys in
-          let bd = kl info (mk_clos e' f) in
+          let bd = kl info tab (mk_clos e' f) in
           List.fold_left (fun b (na,ty) -> mkLambda(na,ty,b)) bd rvtys
       | FLetIn(na,a,b,f,e) ->
           let c = mk_clos (subs_lift e) f in
-          mkLetIn(na, kl info a, kl info b, kl info c)
+          mkLetIn(na, kl info tab a, kl info tab b, kl info tab c)
       | FProd(na,dom,rng) ->
-          mkProd(na, kl info dom, kl info rng)
+          mkProd(na, kl info tab dom, kl info tab rng)
       | FCoFix((n,(na,tys,bds)),e) ->
           let ftys = CArray.Fun1.map mk_clos e tys in
           let fbds =
             CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
-          mkCoFix(n,(na, CArray.Fun1.map kl info ftys, CArray.Fun1.map kl info fbds))
+          mkCoFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds))
       | FFix((n,(na,tys,bds)),e) ->
           let ftys = CArray.Fun1.map mk_clos e tys in
           let fbds =
             CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
-          mkFix(n,(na, CArray.Fun1.map kl info ftys, CArray.Fun1.map kl info fbds))
+          mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds))
       | FEvar((i,args),env) ->
-          mkEvar(i, Array.map (fun a -> kl info (mk_clos env a)) args)
+          mkEvar(i, Array.map (fun a -> kl info tab (mk_clos env a)) args)
       | FProj (p,c) ->
-          mkProj (p, kl info c)
+          mkProj (p, kl info tab c)
       | FLOCKED | FRel _ | FAtom _ | FCast _ | FFlex _ | FInd _ | FConstruct _
         | FApp _ | FCaseT _ | FLIFT _ | FCLOS _ -> term_of_fconstr m
 
 (* Initialization and then normalization *)
 
 (* weak reduction *)
-let whd_val info v =
-  with_stats (lazy (term_of_fconstr (kh info v [])))
+let whd_val info tab v =
+  with_stats (lazy (term_of_fconstr (kh info tab v [])))
 
 (* strong reduction *)
-let norm_val info v =
-  with_stats (lazy (kl info v))
+let norm_val info tab v =
+  with_stats (lazy (kl info tab v))
 
 let inject c = mk_clos (subs_id 0) c
 
-let whd_stack infos m stk =
-  let k = kni infos m stk in
+let whd_stack infos tab m stk =
+  let k = kni infos tab m stk in
   let () = if !share then ignore (fapp_stack k) in (* to unlock Zupdates! *)
   k
 
@@ -1059,7 +1061,10 @@ let whd_stack infos m stk =
 type clos_infos = fconstr infos
 
 let create_clos_infos ?(evars=fun _ -> None) flgs env =
-  create (fun _ -> inject) flgs env evars
+  create (fun _ _ c -> inject c) flgs env evars
+
+let create_tab () = KeyTable.create 17
+
 let oracle_of_infos infos = Environ.oracle infos.i_cache.i_env
 
 let env_of_infos infos = infos.i_cache.i_env
@@ -1067,14 +1072,14 @@ let env_of_infos infos = infos.i_cache.i_env
 let infos_with_reds infos reds =
   { infos with i_flags = reds }
 
-let unfold_reference info key =
+let unfold_reference info tab key =
   match key with
   | ConstKey (kn,_) ->
     if red_set info.i_flags (fCONST kn) then
-      ref_value_cache info key
+      ref_value_cache info tab key
     else None
   | VarKey i ->
     if red_set info.i_flags (fVAR i) then
-      ref_value_cache info key
+      ref_value_cache info tab key
     else None
-  | _ -> ref_value_cache info key
+  | _ -> ref_value_cache info tab key
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index b9c71d72a..3a7f77d52 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -100,13 +100,15 @@ val unfold_red : evaluable_global_reference -> reds
 type table_key = Constant.t Univ.puniverses tableKey
 
 type 'a infos_cache
+type 'a infos_tab
 type 'a infos = {
   i_flags : reds;
   i_cache : 'a infos_cache }
 
-val ref_value_cache: 'a infos -> table_key -> 'a option
-val create: ('a infos -> constr -> 'a) -> reds -> env ->
+val ref_value_cache: 'a infos -> 'a infos_tab -> table_key -> 'a option
+val create: ('a infos -> 'a infos_tab -> constr -> 'a) -> reds -> env ->
   (existential -> constr option) -> 'a infos
+val create_tab : unit -> 'a infos_tab
 val evar_value : 'a infos_cache -> existential -> constr option
 
 val info_env : 'a infos -> env
@@ -200,15 +202,15 @@ val infos_with_reds : clos_infos -> reds -> clos_infos
 (** Reduction function *)
 
 (** [norm_val] is for strong normalization *)
-val norm_val : clos_infos -> fconstr -> constr
+val norm_val : clos_infos -> fconstr infos_tab -> fconstr -> constr
 
 (** [whd_val] is for weak head normalization *)
-val whd_val : clos_infos -> fconstr -> constr
+val whd_val : clos_infos -> fconstr infos_tab -> fconstr -> constr
 
 (** [whd_stack] performs weak head normalization in a given stack. It
    stops whenever a reduction is blocked. *)
 val whd_stack :
-  clos_infos -> fconstr -> stack -> fconstr * stack
+  clos_infos -> fconstr infos_tab -> 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
@@ -225,7 +227,7 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack ->
 (** Conversion auxiliary functions to do step by step normalisation *)
 
 (** [unfold_reference] unfolds references in a [fconstr] *)
-val unfold_reference : clos_infos -> table_key -> fconstr option
+val unfold_reference : clos_infos -> fconstr infos_tab -> table_key -> fconstr option
 
 val eq_table_key : table_key -> table_key -> bool
 
@@ -241,9 +243,9 @@ val mk_clos_deep :
   (fconstr subs -> constr -> fconstr) ->
    fconstr subs -> constr -> fconstr
 
-val kni: clos_infos -> fconstr -> stack -> fconstr * stack
-val knr: clos_infos -> fconstr -> stack -> fconstr * stack
-val kl : clos_infos -> fconstr -> constr
+val kni: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
+val knr: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack
+val kl : clos_infos -> fconstr infos_tab -> fconstr -> constr
 
 val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index b3e689414..2e59fcc18 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -117,12 +117,12 @@ let whd_betaiota env t =
     | App (c, _) ->
       begin match kind c with
       | Ind _ | Construct _ | Evar _ | Meta _ | Const _ | LetIn _ -> t
-      | _ -> whd_val (create_clos_infos betaiota env) (inject t)
+      | _ -> whd_val (create_clos_infos betaiota env) (create_tab ()) (inject t)
       end
-    | _ -> whd_val (create_clos_infos betaiota env) (inject t)
+    | _ -> whd_val (create_clos_infos betaiota env) (create_tab ()) (inject t)
 
 let nf_betaiota env t =
-  norm_val (create_clos_infos betaiota env) (inject t)
+  norm_val (create_clos_infos betaiota env) (create_tab ()) (inject t)
 
 let whd_betaiotazeta env x =
   match kind x with
@@ -133,10 +133,10 @@ let whd_betaiotazeta env x =
       | Ind _ | Construct _ | Evar _ | Meta _ | Const _ -> x
       | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
         | Case _ | Fix _ | CoFix _ | Proj _ ->
-         whd_val (create_clos_infos betaiotazeta env) (inject x)
+         whd_val (create_clos_infos betaiotazeta env) (create_tab ()) (inject x)
       end
     | Rel _ | Cast _ | LetIn _ | Case _ | Proj _ ->
-        whd_val (create_clos_infos betaiotazeta env) (inject x)
+        whd_val (create_clos_infos betaiotazeta env) (create_tab ()) (inject x)
 
 let whd_all env t =
   match kind t with
@@ -147,10 +147,10 @@ let whd_all env t =
       | Ind _ | Construct _ | Evar _ | Meta _ -> t
       | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | LetIn _ | App _
         | Const _ |Case _ | Fix _ | CoFix _ | Proj _ ->
-         whd_val (create_clos_infos all env) (inject t)
+         whd_val (create_clos_infos all env) (create_tab ()) (inject t)
       end
     | Rel _ | Cast _ | LetIn _ | Case _ | Proj _ | Const _ | Var _ ->
-        whd_val (create_clos_infos all env) (inject t)
+        whd_val (create_clos_infos all env) (create_tab ()) (inject t)
 
 let whd_allnolet env t =
   match kind t with
@@ -161,10 +161,10 @@ let whd_allnolet env t =
       | Ind _ | Construct _ | Evar _ | Meta _ | LetIn _ -> t
       | Sort _ | Rel _ | Var _ | Cast _ | Prod _ | Lambda _ | App _
         | Const _ | Case _ | Fix _ | CoFix _ | Proj _ ->
-         whd_val (create_clos_infos allnolet env) (inject t)
+         whd_val (create_clos_infos allnolet env) (create_tab ()) (inject t)
       end
     | Rel _ | Cast _ | Case _ | Proj _ | Const _ | Var _ ->
-        whd_val (create_clos_infos allnolet env) (inject t)
+        whd_val (create_clos_infos allnolet env) (create_tab ()) (inject t)
 
 (********************************************************************)
 (*                         Conversion                               *)
@@ -316,46 +316,16 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
     cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv
   else raise NotConvertible
 
-let rec no_arg_available = function
-  | [] -> true
-  | Zupdate _ :: stk -> no_arg_available stk
-  | Zshift _ :: stk -> no_arg_available stk
-  | Zapp v :: stk -> Int.equal (Array.length v) 0 && no_arg_available stk
-  | Zproj _ :: _ -> true
-  | ZcaseT _ :: _ -> true
-  | Zfix _ :: _ -> true
-
-let rec no_nth_arg_available n = function
-  | [] -> true
-  | Zupdate _ :: stk -> no_nth_arg_available n stk
-  | Zshift _ :: stk -> no_nth_arg_available n stk
-  | Zapp v :: stk ->
-      let k = Array.length v in
-      if n >= k then no_nth_arg_available (n-k) stk
-      else false
-  | Zproj _ :: _ -> true
-  | ZcaseT _ :: _ -> true
-  | Zfix _ :: _ -> true
-
-let rec no_case_available = function
-  | [] -> true
-  | Zupdate _ :: stk -> no_case_available stk
-  | Zshift _ :: stk -> no_case_available stk
-  | Zapp _ :: stk -> no_case_available stk
-  | Zproj (_,_,p) :: _ -> false
-  | ZcaseT _ :: _ -> false
-  | Zfix _ :: _ -> true
-
-let in_whnf (t,stk) =
-  match fterm_of t with
-    | (FLetIn _ | FCaseT _ | FApp _ 
-	  | FCLOS _ | FLIFT _ | FCast _) -> false
-    | FLambda _ -> no_arg_available stk
-    | FConstruct _ -> no_case_available stk
-    | FCoFix _ -> no_case_available stk
-    | FFix(((ri,n),(_,_,_)),_) -> no_nth_arg_available ri.(n) stk
-    | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _ | FProj _) -> true
-    | FLOCKED -> assert false
+type conv_tab = {
+  cnv_inf : clos_infos;
+  lft_tab : fconstr infos_tab;
+  rgt_tab : fconstr infos_tab;
+}
+(** Invariant: for any tl ∈ lft_tab and tr ∈ rgt_tab, there is no mutable memory
+    location contained both in tl and in tr. *)
+
+(** The same heap separation invariant must hold for the fconstr arguments
+    passed to each respective side of the conversion function below. *)
 
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
@@ -365,15 +335,10 @@ let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
 and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
   Control.check_for_interrupt ();
   (* First head reduce both terms *)
-  let whd = whd_stack (infos_with_reds infos betaiotazeta) in
-  let rec whd_both (t1,stk1) (t2,stk2) =
-    let st1' = whd t1 stk1 in
-    let st2' = whd t2 stk2 in
-    (* Now, whd_stack on term2 might have modified st1 (due to sharing),
-       and st1 might not be in whnf anymore. If so, we iterate ccnv. *)
-    if in_whnf st1' then (st1',st2') else whd_both st1' st2' in
-  let ((hd1,v1),(hd2,v2)) = whd_both st1 st2 in
-  let appr1 = (lft1,(hd1,v1)) and appr2 = (lft2,(hd2,v2)) in
+  let ninfos = infos_with_reds infos.cnv_inf betaiotazeta in
+  let (hd1, v1 as appr1) = whd_stack ninfos infos.lft_tab (fst st1) (snd st1) in
+  let (hd2, v2 as appr2) = whd_stack ninfos infos.rgt_tab (fst st2) (snd st2) in
+  let appr1 = (lft1, appr1) and appr2 = (lft2, appr2) in
   (** We delay the computation of the lifts that apply to the head of the term
       with [el_stack] inside the branches where they are actually used. *)
   match (fterm_of hd1, fterm_of hd2) with
@@ -383,7 +348,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	   | (Sort s1, Sort s2) ->
 	       if not (is_empty_stack v1 && is_empty_stack v2) then
 		 anomaly (Pp.str "conversion was given ill-typed terms (Sort).");
-	       sort_cmp_universes (env_of_infos infos) cv_pb s1 s2 cuniv
+              sort_cmp_universes (env_of_infos infos.cnv_inf) cv_pb s1 s2 cuniv
 	   | (Meta n, Meta m) ->
                if Int.equal n m
                then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
@@ -410,24 +375,24 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     (* 2 constants, 2 local defined vars or 2 defined rels *)
     | (FFlex fl1, FFlex fl2) ->
       (try
-	 let cuniv = conv_table_key infos fl1 fl2 cuniv in
+          let cuniv = conv_table_key infos.cnv_inf fl1 fl2 cuniv in
            convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
        with NotConvertible | Univ.UniverseInconsistency _ ->
            (* else the oracle tells which constant is to be expanded *)
-	 let oracle = CClosure.oracle_of_infos infos in
+         let oracle = CClosure.oracle_of_infos infos.cnv_inf in
          let (app1,app2) =
            if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then
-	     match unfold_reference infos fl1 with
+             match unfold_reference infos.cnv_inf infos.lft_tab fl1 with
              | Some def1 -> ((lft1, (def1, v1)), appr2)
              | None ->
-               (match unfold_reference infos fl2 with
+               (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with
                | Some def2 -> (appr1, (lft2, (def2, v2)))
 	       | None -> raise NotConvertible)
            else
-	     match unfold_reference infos fl2 with
+             match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with
              | Some def2 -> (appr1, (lft2, (def2, v2)))
              | None ->
-               (match unfold_reference infos fl1 with
+               (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with
                | Some def1 -> ((lft1, (def1, v1)), appr2)
 	       | None -> raise NotConvertible) 
 	 in
@@ -437,11 +402,11 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
       (* Projections: prefer unfolding to first-order unification,
 	 which will happen naturally if the terms c1, c2 are not in constructor
 	 form *)
-      (match unfold_projection infos p1 with
+      (match unfold_projection infos.cnv_inf p1 with
       | Some s1 ->
         eqappr cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv
       | None ->
-        match unfold_projection infos p2 with
+        match unfold_projection infos.cnv_inf p2 with
         | Some s2 ->
           eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv
 	| None -> 
@@ -455,26 +420,26 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	    raise NotConvertible)
 
     | (FProj (p1,c1), t2) ->
-      (match unfold_projection infos p1 with
+      (match unfold_projection infos.cnv_inf p1 with
       | Some s1 ->
          eqappr cv_pb l2r infos (lft1, (c1, (s1 :: v1))) appr2 cuniv
       | None -> 
 	 (match t2 with 
 	  | FFlex fl2 ->
-	     (match unfold_reference infos fl2 with
+            (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with
               | Some def2 ->
                  eqappr cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
               | None -> raise NotConvertible)
 	  | _ -> raise NotConvertible))
       
     | (t1, FProj (p2,c2)) ->
-      (match unfold_projection infos p2 with
+      (match unfold_projection infos.cnv_inf p2 with
       | Some s2 ->
          eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv
       | None -> 
 	 (match t1 with 
 	  | FFlex fl1 ->
-	     (match unfold_reference infos fl1 with
+            (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with
               | Some def1 ->
                  eqappr cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
               | None -> raise NotConvertible)
@@ -524,37 +489,37 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	
     (* only one constant, defined var or defined rel *)
     | (FFlex fl1, c2)      ->
-       (match unfold_reference infos fl1 with
+       (match unfold_reference infos.cnv_inf infos.lft_tab fl1 with
 	| Some def1 ->
           (** By virtue of the previous case analyses, we know [c2] is rigid.
               Conversion check to rigid terms eventually implies full weak-head
               reduction, so instead of repeatedly performing small-step
               unfoldings, we perform reduction with all flags on. *)
-            let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos)) in
-            let r1 = whd_stack (infos_with_reds infos all) def1 v1 in
+            let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos.cnv_inf)) in
+            let r1 = whd_stack (infos_with_reds infos.cnv_inf all) infos.lft_tab def1 v1 in
             eqappr cv_pb l2r infos (lft1, r1) appr2 cuniv
 	| None -> 
 	   match c2 with
 	   | FConstruct ((ind2,j2),u2) ->
 	      (try
 	      let v2, v1 =
-		eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
+                eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1)
               in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
 	      with Not_found -> raise NotConvertible)
 	   | _ -> raise NotConvertible)
        
     | (c1, FFlex fl2)      ->
-       (match unfold_reference infos fl2 with
+       (match unfold_reference infos.cnv_inf infos.rgt_tab fl2 with
         | Some def2 ->
           (** Symmetrical case of above. *)
-          let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos)) in
-          let r2 = whd_stack (infos_with_reds infos all) def2 v2 in
+          let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos.cnv_inf)) in
+          let r2 = whd_stack (infos_with_reds infos.cnv_inf all) infos.rgt_tab def2 v2 in
           eqappr cv_pb l2r infos appr1 (lft2, r2) cuniv
         | None -> 
 	   match c1 with
 	   | FConstruct ((ind1,j1),u1) ->
  	      (try let v1, v2 =
-	     	     eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
+                    eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2)
                    in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
 	       with Not_found -> raise NotConvertible)
 	   | _ -> raise NotConvertible)
@@ -566,7 +531,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           let cuniv = convert_instances ~flex:false u1 u2 cuniv in
           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else
-          let mind = Environ.lookup_mind (fst ind1) (info_env infos) in
+          let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in
           let nargs = CClosure.stack_args_size v1 in
           if not (Int.equal nargs (CClosure.stack_args_size v2))
           then raise NotConvertible
@@ -581,7 +546,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           let cuniv = convert_instances ~flex:false u1 u2 cuniv in
           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else
-          let mind = Environ.lookup_mind (fst ind1) (info_env infos) in
+          let mind = Environ.lookup_mind (fst ind1) (info_env infos.cnv_inf) in
           let nargs = CClosure.stack_args_size v1 in
           if not (Int.equal nargs (CClosure.stack_args_size v2))
           then raise NotConvertible
@@ -594,14 +559,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     | (FConstruct ((ind1,j1),u1), _) ->
       (try
     	 let v1, v2 =
-    	   eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
+            eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2)
          in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
        with Not_found -> raise NotConvertible)
 
     | (_, FConstruct ((ind2,j2),u2)) ->
       (try
     	 let v2, v1 =
-    	   eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
+            eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1)
          in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
        with Not_found -> raise NotConvertible)
 
@@ -669,6 +634,11 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
 let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
   let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
   let infos = create_clos_infos ~evars reds env in
+  let infos = {
+    cnv_inf = infos;
+    lft_tab = create_tab ();
+    rgt_tab = create_tab ();
+  } in
   ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs
 
 
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index b6bac1a14..99bb8440c 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -90,7 +90,7 @@ let lookup_map map =
 let protect_red map env sigma c0 =
   let evars ev = Evarutil.safe_evar_value sigma ev in
   let c = EConstr.Unsafe.to_constr c0 in
-  EConstr.of_constr (kl (create_clos_infos ~evars all env)
+  EConstr.of_constr (kl (create_clos_infos ~evars all env) (create_tab ())
     (mk_clos_but (lookup_map map sigma c0) (Esubst.subs_id 0) c));;
 
 let protect_tac map =
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 7cfb30f4c..a2155697e 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -134,7 +134,7 @@ let mkSTACK = function
   | STACK(0,v0,stk0), stk -> STACK(0,v0,stack_concat stk0 stk)
   | v,stk -> STACK(0,v,stk)
 
-type cbv_infos = { infos : cbv_value infos; sigma : Evd.evar_map }
+type cbv_infos = { tab : cbv_value infos_tab; infos : cbv_value infos; sigma : Evd.evar_map }
 
 (* Change: zeta reduction cannot be avoided in CBV *)
 
@@ -318,7 +318,7 @@ let rec norm_head info env t stack =
 
 and norm_head_ref k info env stack normt =
   if red_set_ref (info_flags info.infos) normt then
-    match ref_value_cache info.infos normt with
+    match ref_value_cache info.infos info.tab normt with
       | Some body ->
          if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ pr_key normt);
          strip_appl (shift_value k body) stack
@@ -455,8 +455,8 @@ let cbv_norm infos constr =
 (* constant bodies are normalized at the first expansion *)
 let create_cbv_infos flgs env sigma =
   let infos = create
-    (fun old_info c -> cbv_stack_term { infos = old_info; sigma } TOP (subs_id 0) c)
+    (fun old_info tab c -> cbv_stack_term { tab; infos = old_info; sigma } TOP (subs_id 0) c)
     flgs
     env
     (Reductionops.safe_evar_value sigma) in
-  { infos; sigma }
+  { tab = CClosure.create_tab (); infos; sigma }
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index 20883f6f6..eb283a022 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -83,10 +83,12 @@ let infer_table_key infos variances c =
     infer_generic_instance_eq variances u
   | VarKey _ | RelKey _ -> variances
 
+let whd_stack (infos, tab) hd stk = CClosure.whd_stack infos tab hd stk
+
 let rec infer_fterm cv_pb infos variances hd stk =
   Control.check_for_interrupt ();
-  let open CClosure in
   let hd,stk = whd_stack infos hd stk in
+  let open CClosure in
   match fterm_of hd with
   | FAtom a ->
     begin match kind a with
@@ -116,7 +118,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
       if Instance.is_empty u then variances
       else
         let nargs = stack_args_size stk in
-        infer_inductive_instance cv_pb (info_env infos) variances ind nargs u
+        infer_inductive_instance cv_pb (info_env (fst infos)) variances ind nargs u
     in
     infer_stack infos variances stk
   | FConstruct (ctor,u) ->
@@ -124,7 +126,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
       if Instance.is_empty u then variances
       else
         let nargs = stack_args_size stk in
-        infer_constructor_instance_eq (info_env infos) variances ctor nargs u
+        infer_constructor_instance_eq (info_env (fst infos)) variances ctor nargs u
     in
     infer_stack infos variances stk
   | FFix ((_,(_,tys,cl)),e) | FCoFix ((_,(_,tys,cl)),e) ->
@@ -161,7 +163,7 @@ and infer_vect infos variances v =
 
 let infer_term cv_pb env variances c =
   let open CClosure in
-  let infos = create_clos_infos all env in
+  let infos = (create_clos_infos all env, create_tab ()) in
   infer_fterm cv_pb infos variances (CClosure.inject c) []
 
 let infer_arity_constructor is_arity env variances arcn =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 44a69d1c1..0e66ff0b6 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1219,6 +1219,7 @@ let clos_norm_flags flgs env sigma t =
     let evars ev = safe_evar_value sigma ev in
     EConstr.of_constr (CClosure.norm_val
       (CClosure.create_clos_infos ~evars flgs env)
+      (CClosure.create_tab ())
       (CClosure.inject (EConstr.Unsafe.to_constr t)))
   with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term")
 
@@ -1227,6 +1228,7 @@ let clos_whd_flags flgs env sigma t =
     let evars ev = safe_evar_value sigma ev in
     EConstr.of_constr (CClosure.whd_val
       (CClosure.create_clos_infos ~evars flgs env)
+      (CClosure.create_tab ())
       (CClosure.inject (EConstr.Unsafe.to_constr t)))
   with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term")