diff options
| author | Maxime Dénès | 2018-02-24 09:33:03 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-24 09:33:03 +0100 |
| commit | bd41af496fd09d6ecd965190cad2873f1cd6b029 (patch) | |
| tree | 029c44d509cdaba200db07dfed61adb55b237f9e /kernel/environ.ml | |
| parent | c4aeaa7aedb04bf156a4946b05bad8f66d5eec69 (diff) | |
| parent | 557c5a2938f16c0601f5a0323c66b78d2da01ee9 (diff) | |
Merge PR #6784: New IR in VM: Clambda
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 738ecc6e1f..fe5a7dfb57 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -468,7 +468,7 @@ type unsafe_type_judgment = types punsafe_type_judgment (*s Compilation of global declaration *) -let compile_constant_body = Cbytegen.compile_constant_body false +let compile_constant_body = Cbytegen.compile_constant_body ~fail_on_error:false exception Hyp_not_found @@ -560,7 +560,7 @@ let dispatch = it to the name of the coq definition in the reactive retroknowledge) *) let int31_op n op prim kn = { empty_reactive_info with - vm_compiling = Some (Cbytegen.op_compilation n op kn); + vm_compiling = Some (Clambda.compile_prim n op kn); native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn)); } in @@ -599,13 +599,13 @@ fun rk value field -> in { empty_reactive_info with vm_decompile_const = Some int31_decompilation; - vm_before_match = Some Cbytegen.int31_escape_before_match; + vm_before_match = Some Clambda.int31_escape_before_match; native_before_match = Some (Nativelambda.before_match_int31 i31bit_type); } | KInt31 (_, Int31Constructor) -> { empty_reactive_info with - vm_constant_static = Some Cbytegen.compile_structured_int31; - vm_constant_dynamic = Some Cbytegen.dynamic_int31_compilation; + vm_constant_static = Some Clambda.compile_structured_int31; + vm_constant_dynamic = Some Clambda.dynamic_int31_compilation; native_constant_static = Some Nativelambda.compile_static_int31; native_constant_dynamic = Some Nativelambda.compile_dynamic_int31; } |
