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
---
 library/global.ml  | 3 +++
 library/global.mli | 5 +++++
 2 files changed, 8 insertions(+)

(limited to 'library')

diff --git a/library/global.ml b/library/global.ml
index 3b0e504d8a..dac840ddb7 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -158,3 +158,6 @@ let register field value by_clause =
   globalize0 (Safe_typing.register field (kind_of_term value) by_clause)
 
 let register_inline c = globalize0 (Safe_typing.register_inline c)
+
+let set_strategy k l =
+  GlobalSafeEnv.set_safe_env (Safe_typing.set_strategy (safe_env ()) k l)
diff --git a/library/global.mli b/library/global.mli
index c62f51e169..856956a17c 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -105,3 +105,8 @@ val register :
   Retroknowledge.field -> Term.constr -> Term.constr -> unit
 
 val register_inline : constant -> unit
+
+(** {6 Oracle } *)
+
+val set_strategy : 'a Names.tableKey -> Conv_oracle.level -> unit
+
-- 
cgit v1.2.3