Merge branch 'v8.5'

1 files changed, 8 insertions, 2 deletions

diff --git a/kernel/vm.mli b/kernel/vm.mli
index 045d02333c..43a42eb9c4 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -22,7 +22,8 @@ type arguments
 
 type atom =
   | Aid of Vars.id_key
-  | Aind of pinductive
+  | Aind of inductive
+  | Atype of Univ.universe
 
 (** Zippers *)
 
@@ -45,19 +46,24 @@ type whd =
   | Vconstr_const of int
   | Vconstr_block of vblock
   | Vatom_stk of atom * stack
+  | Vuniv_level of Univ.universe_level
+
+val pr_atom : atom -> Pp.std_ppcmds
+val pr_whd : whd -> Pp.std_ppcmds
 
 (** Constructors *)
 
 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 : pconstant -> values
+val val_of_constant : constant -> values
 
 external val_of_annot_switch : annot_switch -> values = "%identity"
 
 (** Destructors *)
 
 val whd_val : values -> whd
+val uni_lvl_val : values -> Univ.universe_level
 
 (** Arguments *)