From 3c5ef2272f02db791cea9f55b65866c2c5a1df95 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Mon, 18 Mar 2013 14:21:36 +0000
Subject: Making local variable warning verbose by default.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16314 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/command.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/command.ml b/toplevel/command.ml
index f8230d63d2..06aa351b5e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -117,7 +117,7 @@ let get_locality id = function
 | Discharge ->
   (** If a Let is defined outside a section, then we consider it as a local definition *)
   let msg = pr_id id ++ strbrk " is declared as a local definition" in
-  let () = if Flags.is_verbose () then msg_warning msg in
+  let () = msg_warning msg in
   true
 | Local -> true
 | Global -> false
-- 
cgit v1.2.3