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.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 351df9d86..7fc3dabcd 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -18,8 +18,8 @@ open Names
val oracle_order : 'a tableKey -> 'a tableKey -> bool
(* Changing the oracle *)
-val set_opaque_const : kernel_name -> unit
-val set_transparent_const : kernel_name -> unit
+val set_opaque_const : constant -> unit
+val set_transparent_const : constant -> unit
val set_opaque_var : identifier -> unit
val set_transparent_var : identifier -> unit