aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativeconv.ml
diff options
context:
space:
mode:
authorMaxime Dénès2016-06-28 13:55:20 +0200
committerMaxime Dénès2016-06-28 13:57:33 +0200
commit0e07e69dae3f3f4a99f824533f54a3991aacac6a (patch)
treef2022d27c1742b3f3e99d76204a51860b6bc6ad5 /kernel/nativeconv.ml
parenteb72574e1b526827706ee06206eb4a9626af3236 (diff)
Revert "A new infrastructure for warnings."
This reverts commit 925d258d7d03674c601a1f3832122b3b4b1bc9b0. I forgot that Jenkins gave me a spurious success when trying to build this PR. There are a few rough edges to fix, so reverting meanwhile. The Jenkins issue has been fixed by Matej. Sorry for the noise.
Diffstat (limited to 'kernel/nativeconv.ml')
-rw-r--r--kernel/nativeconv.ml9
1 files changed, 2 insertions, 7 deletions
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 2f985e15ac..a0ff9e123a 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -145,16 +145,11 @@ let native_conv_gen pb sigma env univs t1 t2 =
end
| _ -> anomaly (Pp.str "Compilation failure")
-let warn_no_native_compiler =
- let open Pp in
- CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler"
- (fun () -> strbrk "Native compiler is disabled," ++
- strbrk " falling back to VM conversion test.")
-
(* Wrapper for [native_conv] above *)
let native_conv cv_pb sigma env t1 t2 =
if Coq_config.no_native_compiler then begin
- warn_no_native_compiler ();
+ let msg = "Native compiler is disabled, falling back to VM conversion test." in
+ Feedback.msg_warning (Pp.str msg);
vm_conv cv_pb env t1 t2
end
else