1 files changed, 18 insertions, 98 deletions
diff --git a/kernel/vm.mli b/kernel/vm.mli
index 6e9579aa..50ebc906 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -1,115 +1,35 @@
-open Names
-open Term
-open Cbytecodes
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+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
-
-(** 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
-  | 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.universe_level
-
-(** For debugging purposes only *)
-
-val pr_atom : atom -> Pp.std_ppcmds
-val pr_whd : whd -> Pp.std_ppcmds
-val pr_stack : stack -> 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 : 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 *)
-
-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 *)