refined the conversion oracle

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10961 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 17 insertions, 12 deletions

diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 6e09ce6f0..86e108c6f 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -10,26 +10,31 @@
 
 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