1 files changed, 8 insertions, 98 deletions
diff --git a/kernel/vm.mli b/kernel/vm.mli
index bc38452d4..c6d92ba26 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -6,118 +6,28 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
-open Constr
-open Cbytecodes
+open Vmvalues
 
 (** Debug printing *)
 
 val set_drawinstr : unit -> unit
 
-(** Machine code *)
-
-type tcode
-
-(** Values *)
-
-type vprod
-type vfun
-type vfix
-type vcofix
-type vblock
-type vswitch
-type arguments
-
-type atom =
-  | Aid of Vars.id_key
-  | Aind of inductive
-  | Atype of Univ.Universe.t
-
-(** Zippers *)
-
-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
-
-type to_up
-
-type whd =
-  | Vsort of Sorts.t
-  | Vprod of vprod
-  | Vfun of vfun
-  | Vfix of vfix * arguments option
-  | Vcofix of vcofix * to_up * arguments option
-  | Vconstr_const of int
-  | Vconstr_block of vblock
-  | Vatom_stk of atom * stack
-  | Vuniv_level of Univ.Level.t
-
-(** For debugging purposes only *)
-
-val pr_atom : atom -> Pp.t
-val pr_whd : whd -> Pp.t
-val pr_stack : stack -> Pp.t
-
-(** 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 : Constant.t -> values
-
-external val_of_annot_switch : annot_switch -> values = "%identity"
-
-(** Destructors *)
-
-val whd_val : values -> whd
-val uni_lvl_val : values -> Univ.Level.t
-
-(** Arguments *)
-
-val nargs : arguments -> int
-val arg : arguments -> int -> values
-
-(** Product *)
-
-val dom : vprod -> values
-val codom : vprod -> vfun
-
-(** Function *)
-
-val body_of_vfun : int -> vfun -> values
-val decompose_vfun2  : int -> vfun -> vfun -> int * values * values
-
-(** 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 *)
 
-(** CoFix *)
-
-val current_cofix : vcofix -> int
-val check_cofix : vcofix -> vcofix -> bool
 val reduce_cofix : int -> vcofix -> values array * values array
                                       (** bodies , types *)
 
-(** Block *)
+val type_of_switch : vswitch -> values
 
-val btag  : vblock -> int
-val bsize : vblock -> int
-val bfield : vblock -> int -> values
+val branch_of_switch : int -> vswitch -> (int * values) array
 
-(** Switch *)
+val reduce_fun : int -> vfun -> values
 
-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
+(** [decompose_vfun2 k f1 f2] takes two functions [f1] and [f2] at current
+    DeBruijn level [k], with [n] lambdas in common, returns [n] and the reduced
+    bodies under those lambdas. *)
+val decompose_vfun2  : int -> vfun -> vfun -> int * values * values
 
 (** Apply a value *)