From 0e07e69dae3f3f4a99f824533f54a3991aacac6a Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 28 Jun 2016 13:55:20 +0200
Subject: 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.
---
 pretyping/classops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/classops.ml')

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index d3d4201f57..55220f44c0 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -387,7 +387,7 @@ let add_coercion_in_graph (ic,source,target) =
   end;
   let is_ambig = match !ambig_paths with [] -> false | _ -> true in
   if is_ambig && is_verbose () then
-    Feedback.msg_info (message_ambig !ambig_paths)
+    Feedback.msg_warning (message_ambig !ambig_paths)
 
 type coercion = {
   coercion_type   : coe_typ;
-- 
cgit v1.2.3