diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2014-04-06 12:41:26 -0400 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2014-04-09 01:05:48 -0400 |
| commit | aa3b8b7b24e809b379fcc86f2b21ae4380b211d5 (patch) | |
| tree | 254b9d84ee42798a513bcd5aea032a6e552b2067 /kernel/environ.ml | |
| parent | de61c7d77e49286622c4aebd56f2e87b0df93903 (diff) | |
Partial support for open terms in int31.
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 4c1d9bddc..4ce42c919 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -465,7 +465,13 @@ let register = let rk = add_vm_constant_static_info retroknowledge c Cbytegen.compile_structured_int31 in - add_vm_constant_dynamic_info rk c Cbytegen.dynamic_int31_compilation + let rk = + add_vm_constant_dynamic_info rk c Cbytegen.dynamic_int31_compilation + in + let rk = + add_native_constant_static_info rk c Nativelambda.compile_static_int31 + in + add_native_constant_dynamic_info rk c Nativelambda.compile_dynamic_int31 in (* subfunction which adds the compiling information of an |