From 16c884413bbf2f0b5fb43bd0be7da0bf7c5e4e75 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 13 Feb 2018 17:49:21 +0100
Subject: Pass the constant cache as a separate argument in kernel reduction.

---
 pretyping/cbv.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'pretyping/cbv.ml')

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index e42576d95b..1718269b48 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -132,7 +132,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 *)
 
@@ -316,7 +316,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
@@ -453,8 +453,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 }
-- 
cgit v1.2.3