Imported Upstream version 8.5~beta1+dfsg

1 files changed, 5 insertions, 12 deletions

diff --git a/kernel/vm.mli b/kernel/vm.mli
index 58228eb8..295ea83c 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -1,7 +1,6 @@
 open Names
 open Term
 open Cbytecodes
-open Cemitcodes
 
 (** Efficient Virtual Machine *)
 
@@ -25,9 +24,9 @@ type vswitch
 type arguments
 
 type atom =
-  | Aid of id_key
-  | Aiddef of id_key * values
-  | Aind of inductive
+  | Aid of Vars.id_key
+  | Aiddef of Vars.id_key * values
+  | Aind of pinductive
 
 (** Zippers *)
 
@@ -53,15 +52,9 @@ type whd =
 (** Constructors *)
 
 val val_of_str_const : structured_constant -> values
-
 val val_of_rel : int -> values
-val val_of_rel_def : int -> values -> values
-
-val val_of_named : identifier -> values
-val val_of_named_def : identifier -> values -> values
-
-val val_of_constant : constant -> values
-val val_of_constant_def : int -> constant -> values -> values
+val val_of_named : Id.t -> values
+val val_of_constant : pconstant -> values
 
 external val_of_annot_switch : annot_switch -> values = "%identity"