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/environ.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel/environ.ml')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index ae6817a76d..9f18680046 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -38,6 +38,8 @@ type env = Pre_env.env
 
 let pre_env env = env
 let env_of_pre_env env = env
+let oracle env = env.env_conv_oracle
+let set_oracle env o = { env with env_conv_oracle = o }
 
 let empty_named_context_val = empty_named_context_val
 
-- 
cgit v1.2.3