diff options
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 710bfa19b8..30a346c910 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -676,18 +676,12 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta 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 -> Term.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 (); + Feedback.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion"); gen_conv cv_pb env t1 t2 let default_conv cv_pb ?(l2r=false) env t1 t2 = |