From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 25 Jul 2008 15:12:53 +0200
Subject: Imported Upstream version 8.2~beta3+dfsg

---
 kernel/conv_oracle.mli | 31 ++++++++++++++++++-------------
 1 file changed, 18 insertions(+), 13 deletions(-)

(limited to 'kernel/conv_oracle.mli')

diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 966edd1d..6a774b4b 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -6,30 +6,35 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: conv_oracle.mli 6621 2005-01-21 17:24:37Z herbelin $ i*)
+(*i $Id: conv_oracle.mli 10961 2008-05-21 23:26:23Z barras $ i*)
 
 open Names
 
-
 (* 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 : 'a tableKey -> 'a tableKey -> bool
 
-(* Changing the oracle *)
-val set_opaque_const      : constant -> unit
-val set_transparent_const : constant -> unit
+(* Priority for the expansion of constant in the conversion test.
+ * Higher levels means that the expansion is less prioritary.
+ * (And Expand stands for -oo, and Opaque +oo.)
+ * The default value (transparent constants) is [Level 0].
+ *)
+type level = Expand | Level of int | Opaque
+val transparent : level
 
-val set_opaque_var      : identifier -> unit
-val set_transparent_var : identifier -> unit
+val get_strategy : 'a tableKey -> level
 
-val is_opaque_cst : constant -> bool
-val is_opaque_var : identifier -> bool
+(* Sets the level of a constant.
+ * Level of RelKey constant cannot be set. *)
+val set_strategy : 'a tableKey -> level -> unit
 
-(*****************************)
+val get_transp_state : unit -> transparent_state
 
-(* transparent state summary operations *)
+(*****************************)
+(* Summary operations *)
+type oracle
 val init     : unit -> unit
-val freeze   : unit -> transparent_state
-val unfreeze : transparent_state -> unit
+val freeze   : unit -> oracle
+val unfreeze : oracle -> unit
-- 
cgit v1.2.3