diff options
| author |  Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:28 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:28 -0500 |
| commit | 1ef7f1c0c6897535a86daa77799714e25638f5e9 (patch) | |
| tree | 5bcca733632ecc84d2c6b1ee48cb2e557a7adba5 /kernel/clambda.mli | |
| parent | 3a2fac7bcee36fd9dcb4f39a615c8ac0349abcc9 (diff) | |
| parent | 9ebf44d84754adc5b64fcf612c6816c02c80462d (diff) | |
Updated version 8.9.0 from 'upstream/8.9.0'
with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63
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 |