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.
---
 plugins/syntax/nat_syntax.ml | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

(limited to 'plugins/syntax')

diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 89305838b1..3142c8cf00 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -26,16 +26,14 @@ open Errors
 
 let threshold = of_int 5000
 
-let warn_large_nat =
-  CWarnings.create ~name:"large-nat" ~category:"numbers"
-    (fun () -> strbrk "Stack overflow or segmentation fault happens when " ++
-                 strbrk "working with large numbers in nat (observed threshold " ++
-                 strbrk "may vary from 5000 to 70000 depending on your system " ++
-                 strbrk "limits and on the command executed).")
-
 let nat_of_int dloc n =
   if is_pos_or_zero n then begin
-      if less_than threshold n then warn_large_nat ();
+      if less_than threshold n then
+	Feedback.msg_warning
+	  (strbrk "Stack overflow or segmentation fault happens when " ++
+	   strbrk "working with large numbers in nat (observed threshold " ++
+	   strbrk "may vary from 5000 to 70000 depending on your system " ++
+	   strbrk "limits and on the command executed).");
       let ref_O = GRef (dloc, glob_O, None) in
       let ref_S = GRef (dloc, glob_S, None) in
       let rec mk_nat acc n =
-- 
cgit v1.2.3