diff options
| author | Maxime Dénès | 2014-04-06 12:41:26 -0400 |
|---|---|---|
| committer | Maxime Dénès | 2014-04-09 01:05:48 -0400 |
| commit | aa3b8b7b24e809b379fcc86f2b21ae4380b211d5 (patch) | |
| tree | 254b9d84ee42798a513bcd5aea032a6e552b2067 /kernel/nativelambda.mli | |
| parent | de61c7d77e49286622c4aebd56f2e87b0df93903 (diff) | |
Partial support for open terms in int31.
Diffstat (limited to 'kernel/nativelambda.mli')
| -rw-r--r-- | kernel/nativelambda.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index d4be2279d3..b97e010061 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -29,3 +29,8 @@ val mk_lazy : lambda -> lambda val get_allias : env -> constant -> constant val lambda_of_constr : env -> evars -> Constr.constr -> lambda + +val compile_static_int31 : bool -> Constr.constr array -> lambda + +val compile_dynamic_int31 : bool -> Nativeinstr.prefix -> Names.constructor -> + Nativeinstr.lambda array -> Nativeinstr.lambda |