From 7f9223bf9939a626b0813ecc6c34b4ef19b123f0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 14 Jan 2018 01:14:27 +0100
Subject: Store the conversion oracle in constant and inductive definitions.

We also have to update the checker to deserialize this additional data,
but it is not using it in type-checking yet.
---
 kernel/pre_env.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'kernel/pre_env.ml')

diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index c5254b453a..4ef89f8c0e 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -75,7 +75,6 @@ type env = {
   env_nb_rel        : int;
   env_stratification : stratification;
   env_typing_flags  : typing_flags;
-  env_conv_oracle   : Conv_oracle.oracle;
   retroknowledge : Retroknowledge.retroknowledge;
   indirect_pterms : Opaqueproof.opaquetab;
 }
@@ -98,8 +97,7 @@ let empty_env = {
   env_stratification = {
     env_universes = UGraph.initial_universes;
     env_engagement = PredicativeSet };
-  env_typing_flags = Declareops.safe_flags;
-  env_conv_oracle = Conv_oracle.empty;
+  env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
   retroknowledge = Retroknowledge.initial_retroknowledge;
   indirect_pterms = Opaqueproof.empty_opaquetab }
 
-- 
cgit v1.2.3