From b7033be417da7b84a2fe723e02bf3c4efc55e6b0 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 30 Nov 2011 10:36:18 +0000
Subject: Preventing Implicit Arguments warning to be shown in non verbose mode
 + flushing printing of the message .

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

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 422da85447..5cd67a8b0e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -421,7 +421,8 @@ GEXTEND Gram
       | IDENT "Include"; e = module_expr_inl; l = LIST0 ext_module_expr ->
 	  VernacInclude(e::l)
       | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type ->
-	  warning "Include Type is deprecated; use Include instead";
+	  Flags.if_verbose
+            msg_warning (str "Include Type is deprecated; use Include instead");
           VernacInclude(e::l) ] ]
   ;
   export_token:
-- 
cgit v1.2.3