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

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 40f16a6e6d..3132d45e37 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -777,3 +777,7 @@ environment, and store for the future (instead of just its type)
 loaded by side-effect once and for all (like it is done in OCaml).
 Would this be correct with respect to undo's and stuff ?
 *)
+
+let set_strategy e k l = { e with env =
+   (Environ.set_oracle e.env
+      (Conv_oracle.set_strategy (Environ.oracle e.env) k l)) }
-- 
cgit v1.2.3