diff options
Diffstat (limited to 'kernel/clambda.mli')
| -rw-r--r-- | kernel/clambda.mli | 9 |
1 files changed, 5 insertions, 4 deletions
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 |