aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/conv_oracle.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/conv_oracle.mli')
-rw-r--r--kernel/conv_oracle.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index f875fabf2..2a6db4b4b 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -22,6 +22,9 @@ val oracle_order : bool -> 'a tableKey -> 'a tableKey -> bool
type level = Expand | Level of int | Opaque
val transparent : level
+(** Check whether a level is transparent *)
+val is_transparent : level -> bool
+
val get_strategy : 'a tableKey -> level
(** Sets the level of a constant.