From c47b205206d832430fa80a3386be80149e281d33 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Fri, 9 Oct 2015 13:04:56 +0200
Subject: Code cleaning in VM (with Benjamin).

Rename some functions, remove dead code related to (previously deprecated, now
removed) option Set Boxed Values.
---
 kernel/vm.mli | 14 +++-----------
 1 file changed, 3 insertions(+), 11 deletions(-)

(limited to 'kernel/vm.mli')

diff --git a/kernel/vm.mli b/kernel/vm.mli
index d31448ee1..045d02333 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,7 +22,6 @@ type arguments
 
 type atom =
   | Aid of Vars.id_key
-  | Aiddef of Vars.id_key * values
   | Aind of pinductive
 
 (** Zippers *)
@@ -106,10 +102,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