From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 21 Nov 2006 21:38:49 +0000 Subject: Imported Upstream version 8.1~gamma --- kernel/vconv.mli | 25 +------------------------ 1 file changed, 1 insertion(+), 24 deletions(-) (limited to 'kernel/vconv.mli') diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 4aed5d05..551615aa 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -19,28 +19,5 @@ val use_vm : unit -> bool val set_use_vm : bool -> unit val vconv : conv_pb -> types conversion_function -(***********************************************************************) -(*s Reduction functions *) -val cbv_vm : env -> constr -> types -> constr - - - - - -val nf_val : env -> values -> types -> constr - -val nf_whd : env -> Vm.whd -> types -> constr - -val nf_stk : env -> constr -> types -> Vm.stack -> constr - -val nf_args : env -> Vm.arguments -> types -> types * constr array - -val nf_bargs : env -> Vm.vblock -> types -> constr array - -val nf_fun : env -> Vm.vfun -> types -> constr - -val nf_fix : env -> Vm.vfix -> constr - -val nf_cofix : env -> Vm.vcofix -> constr +val val_of_constr : env -> constr -> values - -- cgit v1.2.3