From aa3b8b7b24e809b379fcc86f2b21ae4380b211d5 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sun, 6 Apr 2014 12:41:26 -0400 Subject: Partial support for open terms in int31. --- kernel/nativelambda.mli | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'kernel/nativelambda.mli') diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index d4be2279d..b97e01006 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 -- cgit v1.2.3