From dbd94e12c9c6cb0fdecb44bfedacf0c4ae50bc3e Mon Sep 17 00:00:00 2001
From: gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>
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/conv_oracle.mli | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

(limited to 'kernel/conv_oracle.mli')

diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 7bb62112c..24797238d 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -8,11 +8,15 @@
 
 open Names
 
+type oracle
+
+val empty : oracle
+
 (** Order on section paths for unfolding.
    If [oracle_order kn1 kn2] is true, then unfold kn1 first.
    Note: the oracle does not introduce incompleteness, it only
    tries to postpone unfolding of "opaque" constants. *)
-val oracle_order : bool -> 'a tableKey -> 'a tableKey -> bool
+val oracle_order : oracle -> bool -> 'a tableKey -> 'a tableKey -> bool
 
 (** Priority for the expansion of constant in the conversion test.
  * Higher levels means that the expansion is less prioritary.
@@ -25,16 +29,11 @@ val transparent : level
 (** Check whether a level is transparent *)
 val is_transparent : level -> bool
 
-val get_strategy : 'a tableKey -> level
+val get_strategy : oracle -> 'a tableKey -> level
 
 (** Sets the level of a constant.
  * Level of RelKey constant cannot be set. *)
-val set_strategy : 'a tableKey -> level -> unit
+val set_strategy : oracle -> 'a tableKey -> level -> oracle
 
-val get_transp_state : unit -> transparent_state
+val get_transp_state : oracle -> transparent_state
 
-(****************************
-   Summary operations *)
-type oracle
-val freeze   : [ `Yes | `No | `Shallow ] -> oracle
-val unfreeze : oracle -> unit
-- 
cgit v1.2.3