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.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'kernel/pre_env.mli')

diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 054ae17437..fef530c872 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -53,7 +53,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;
 }
-- 
cgit v1.2.3