aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/vm.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/vm.mli')
-rw-r--r--kernel/vm.mli8
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/vm.mli b/kernel/vm.mli
index fa88418ce..295ea83c4 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -24,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 *)
@@ -54,7 +54,7 @@ type whd =
val val_of_str_const : structured_constant -> values
val val_of_rel : int -> values
val val_of_named : Id.t -> values
-val val_of_constant : constant -> values
+val val_of_constant : pconstant -> values
external val_of_annot_switch : annot_switch -> values = "%identity"