From f045db6a3a8efc08d6db7fc58e5a59d786099555 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 30 Nov 2011 10:55:17 +0000
Subject: Continuing r14747 being actually incomplete (flushing warnings and
 printing them only if verbose).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14750 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_vernac.ml4 | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 5cd67a8b0e..2dc72f658f 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -627,14 +627,16 @@ GEXTEND Gram
      (* moved there so that camlp5 factors it with the previous rule *)
      | IDENT "Arguments"; IDENT "Scope"; qid = smart_global;
        "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" ->
-         warning "Arguments Scope is deprecated; use Arguments instead";
+	   Flags.if_verbose
+             msg_warning (str "Arguments Scope is deprecated; use Arguments instead");
 	 VernacArgumentsScope (use_section_locality (),qid,scl)
 
       (* Implicit *)
       | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global;
 	   pos = LIST0 [ "["; l = LIST0 implicit_name; "]" ->
 	     List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
-	   warning "Implicit Arguments is deprecated; use Arguments instead";
+	   Flags.if_verbose
+             msg_warning (str "Implicit Arguments is deprecated; use Arguments instead");
 	   VernacDeclareImplicits (use_section_locality (),qid,pos)
 
       | IDENT "Implicit"; "Type"; bl = reserv_list ->
-- 
cgit v1.2.3