From f7a82d5f7edcce7ef70b99a10b92d8dcd5cfea70 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 24 Feb 2007 15:22:07 +0000
Subject: Une passe sur les warnings (ajout Options.warn déclenchée par
 compile-verbose + ajout Pp.strbrk pour faciliter les césures faciles +
 messages divers).

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

(limited to 'toplevel/command.ml')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index d9c91808f7..739a7b47f7 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -144,8 +144,9 @@ let declare_definition ident (local,boxed,dok) bl red_option c typopt hook =
         let _ = declare_variable ident (Lib.cwd(),c,IsDefinition Definition) in
         definition_message ident;
         if Pfedit.refining () then 
-          msgerrnl (str"Warning: Local definition " ++ pr_id ident ++ 
-          str" is not visible from current goals");
+          Options.if_verbose msg_warning 
+	    (str"Local definition " ++ pr_id ident ++ 
+             str" is not visible from current goals");
         VarRef ident
     | (Global|Local) ->
         declare_global_definition ident ce' local in
-- 
cgit v1.2.3