From dbd94e12c9c6cb0fdecb44bfedacf0c4ae50bc3e Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 31 Oct 2013 14:24:43 +0000
Subject: Conv_orable made functional and part of pre_env

But for vm, the kernel should be functional now

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16961 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/pre_env.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/pre_env.ml')

diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 9a2bb73d1f..e543c4e687 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -54,6 +54,7 @@ type env = {
   env_rel_val       : lazy_val list;
   env_nb_rel        : int;
   env_stratification : stratification;
+  env_conv_oracle   : Conv_oracle.oracle;
   retroknowledge : Retroknowledge.retroknowledge }
 
 type named_context_val = named_context * named_vals
@@ -74,6 +75,7 @@ let empty_env = {
   env_stratification = {
     env_universes = initial_universes;
     env_engagement = None };
+  env_conv_oracle = Conv_oracle.empty;
   retroknowledge = Retroknowledge.initial_retroknowledge }
 
 
@@ -118,6 +120,7 @@ let push_named d env =
     env_rel_val = env.env_rel_val;
     env_nb_rel = env.env_nb_rel;
     env_stratification = env.env_stratification;
+    env_conv_oracle = env.env_conv_oracle;
     retroknowledge = env.retroknowledge; }
 
 let lookup_named_val id env =
-- 
cgit v1.2.3