From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Fri, 13 Nov 2015 11:31:34 +0100
Subject: Imported Upstream version 8.5~beta3+dfsg

---
 kernel/vm.mli | 25 ++++++++++++-------------
 1 file changed, 12 insertions(+), 13 deletions(-)

(limited to 'kernel/vm.mli')

diff --git a/kernel/vm.mli b/kernel/vm.mli
index 51903568..43a42eb9 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -2,13 +2,10 @@ open Names
 open Term
 open Cbytecodes
 
-(** Efficient Virtual Machine *)
+(** Debug printing *)
 
 val set_drawinstr : unit -> unit
 
-val transp_values : unit -> bool
-val set_transp_values : bool -> unit
-
 (** Machine code *)
 
 type tcode
@@ -25,8 +22,8 @@ type arguments
 
 type atom =
   | Aid of Vars.id_key
-  | Aiddef of Vars.id_key * values
-  | Aind of pinductive
+  | Aind of inductive
+  | Atype of Univ.universe
 
 (** Zippers *)
 
@@ -34,6 +31,7 @@ type zipper =
   | Zapp of arguments
   | Zfix of vfix * arguments  (** might be empty *)
   | Zswitch of vswitch
+  | Zproj of Constant.t (* name of the projection *)
 
 type stack = zipper list
 
@@ -48,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 *)
 
@@ -105,10 +108,6 @@ val case_info : vswitch -> case_info
 val type_of_switch : vswitch -> values
 val branch_of_switch : int -> vswitch -> (int * values) array
 
-(** Evaluation *)
-
-val whd_stack : values -> stack -> whd
-val force_whd : values -> stack -> whd
-
-val eta_whd : int -> whd -> values
+(** Apply a value *)
 
+val apply_whd : int -> whd -> values
-- 
cgit v1.2.3