From 85a223796514d98211c06593d7ec72e56ed21e33 Mon Sep 17 00:00:00 2001 From: barras Date: Wed, 21 May 2008 23:26:23 +0000 Subject: refined the conversion oracle git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10961 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/conv_oracle.mli | 29 +++++++++++++++++------------ 1 file changed, 17 insertions(+), 12 deletions(-) (limited to 'kernel/conv_oracle.mli') 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 -- cgit v1.2.3