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

(limited to 'kernel/pre_env.mli')

diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 10c9c27cb5..f634719f9a 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -46,6 +46,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
-- 
cgit v1.2.3