From e9f511f4f4d9989e4cb6ba290f46ea7dba3089f7 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 28 May 2013 21:57:38 +0000
Subject: Fixing warning of deprecated Argument Scopes.

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

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 004dbab7b4..7a78a7dae2 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -622,9 +622,8 @@ 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 ]; "]" ->
-	   Flags.if_verbose
-             msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead");
-	 VernacArgumentsScope (qid,scl)
+        msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead");
+        VernacArgumentsScope (qid,scl)
 
       (* Implicit *)
       | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global;
-- 
cgit v1.2.3