From 2f2d31d8408b4e15b193110309c4800a456cfb83 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 Apr 2018 13:20:37 +0200
Subject: The cbv reduction does not rely on the kernel info data structure
 anymore.

---
 kernel/reduction.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 00576476ab..18697d07e5 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -316,8 +316,8 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
 
 type conv_tab = {
   cnv_inf : clos_infos;
-  lft_tab : fconstr infos_tab;
-  rgt_tab : fconstr infos_tab;
+  lft_tab : clos_tab;
+  rgt_tab : clos_tab;
 }
 (** Invariant: for any tl ∈ lft_tab and tr ∈ rgt_tab, there is no mutable memory
     location contained both in tl and in tr. *)
@@ -346,7 +346,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.cnv_inf) cv_pb s1 s2 cuniv
+              sort_cmp_universes (info_env 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
-- 
cgit v1.2.3