From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 kernel/vm.mli | 43 +++++++++++++++++++++++++++++--------------
 1 file changed, 29 insertions(+), 14 deletions(-)

(limited to 'kernel/vm.mli')

diff --git a/kernel/vm.mli b/kernel/vm.mli
index 5ecc8d99..58228eb8 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -3,15 +3,18 @@ open Term
 open Cbytecodes
 open Cemitcodes
 
+(** Efficient Virtual Machine *)
 
 val set_drawinstr : unit -> unit
 
 val transp_values : unit -> bool
 val set_transp_values : bool -> unit
-(* le code machine *)
+
+(** Machine code *)
+
 type tcode
 
-(* Les valeurs ***********)
+(** Values *)
 
 type vprod
 type vfun
@@ -26,11 +29,11 @@ type atom =
   | Aiddef of id_key * values
   | Aind of inductive
 
-(* Les zippers *)
+(** Zippers *)
 
 type zipper =
   | Zapp of arguments
-  | Zfix of vfix*arguments  (* Peut-etre vide *)
+  | Zfix of vfix * arguments  (** might be empty *)
   | Zswitch of vswitch
 
 type stack = zipper list
@@ -48,6 +51,7 @@ type whd =
   | Vatom_stk of atom * stack
 
 (** Constructors *)
+
 val val_of_str_const : structured_constant -> values
 
 val val_of_rel : int -> values
@@ -62,45 +66,56 @@ val val_of_constant_def : int -> constant -> values -> values
 external val_of_annot_switch : annot_switch -> values = "%identity"
 
 (** Destructors *)
+
 val whd_val : values -> whd
 
-(* Arguments *)
+(** Arguments *)
+
 val nargs : arguments -> int
 val arg : arguments -> int -> values
 
-(* Product *)
+(** Product *)
+
 val dom : vprod -> values
 val codom : vprod -> vfun
 
-(* Function *)
+(** Function *)
+
 val body_of_vfun : int -> vfun -> values
 val decompose_vfun2  : int -> vfun -> vfun -> int * values * values
 
-(* Fix *)
+(** Fix *)
+
 val current_fix : vfix -> int
 val check_fix : vfix -> vfix -> bool
 val rec_args : vfix -> int array
 val reduce_fix : int -> vfix -> vfun array * values array
-                              (* bodies ,  types *)
+                              (** bodies ,  types *)
+
+(** CoFix *)
 
-(* CoFix *)
 val current_cofix : vcofix -> int
 val check_cofix : vcofix -> vcofix -> bool
 val reduce_cofix : int -> vcofix -> values array * values array
-                                      (* bodies , types *)
-(* Block *)
+                                      (** bodies , types *)
+
+(** Block *)
+
 val btag : vblock -> int
 val bsize : vblock -> int
 val bfield : vblock -> int -> values
 
-(* Switch *)
+(** Switch *)
+
 val check_switch : vswitch -> vswitch -> bool
 val case_info : vswitch -> case_info
 val type_of_switch : vswitch -> values
 val branch_of_switch : int -> vswitch -> (int * values) array
 
-(* Evaluation *)
+(** Evaluation *)
+
 val whd_stack : values -> stack -> whd
 val force_whd : values -> stack -> whd
 
+val eta_whd : int -> whd -> values
 
-- 
cgit v1.2.3