diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-05-15 21:51:21 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-05-28 14:41:39 +0200 |
| commit | b053d98fb17d2f46878f49d7adf4839ae632c10b (patch) | |
| tree | 044bd5fa2380cd0313f1b7cc0d49354be9dc7b4b /kernel/reduction.ml | |
| parent | 5021c6bd8e08fb465152638c9a56108d317002f8 (diff) | |
Remove vm_conv hook and reorganize kernel files
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 18 |
1 files changed, 0 insertions, 18 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 38106fbf6..6cd3917c7 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -789,24 +789,6 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta env univs t1 t2 = infer_conv_universes CUMUL l2r evars ts env univs t1 t2 -(* This reference avoids always having to link C code with the kernel *) -let vm_conv = ref (fun cv_pb env -> - gen_conv cv_pb env ~evars:((fun _->None), universes env)) - -let warn_bytecode_compiler_failed = - let open Pp in - CWarnings.create ~name:"bytecode-compiler-failed" ~category:"bytecode-compiler" - (fun () -> strbrk "Bytecode compiler failed, " ++ - strbrk "falling back to standard conversion") - -let set_vm_conv (f:conv_pb -> types kernel_conversion_function) = vm_conv := f -let vm_conv cv_pb env t1 t2 = - try - !vm_conv cv_pb env t1 t2 - with Not_found | Invalid_argument _ -> - warn_bytecode_compiler_failed (); - gen_conv cv_pb env t1 t2 - let default_conv cv_pb ?(l2r=false) env t1 t2 = gen_conv cv_pb env t1 t2 |