From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- kernel/clambda.mli | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'kernel/clambda.mli') diff --git a/kernel/clambda.mli b/kernel/clambda.mli index 827eb550..8ff10b45 100644 --- a/kernel/clambda.mli +++ b/kernel/clambda.mli @@ -1,13 +1,14 @@ open Names open Cinstr +open Environ exception TooLargeInductive of Pp.t -val lambda_of_constr : optimize:bool -> Pre_env.env -> Constr.t -> lambda +val lambda_of_constr : optimize:bool -> env -> Constr.t -> lambda val decompose_Llam : lambda -> Name.t array * lambda -val get_alias : Pre_env.env -> Constant.t -> Constant.t +val get_alias : env -> Constant.t -> Constant.t val compile_prim : int -> Cbytecodes.instruction -> Constr.pconstant -> bool -> lambda array -> lambda @@ -26,5 +27,5 @@ val dynamic_int31_compilation : bool -> lambda array -> lambda matching integers (in case they are in processor representation) *) val int31_escape_before_match : bool -> lambda -> lambda -val eta_expand : (Pre_env.env -> Constr.t -> Constr.types -> Constr.t) Hook.value -val eta_expand_hook : (Pre_env.env -> Constr.t -> Constr.types -> Constr.t) Hook.t +(** Dump the VM lambda code after compilation (for debugging purposes) *) +val dump_lambda : bool ref -- cgit v1.2.3