From fa04b2438319c763ac6d1fd07ecdfd47a0663b2c Mon Sep 17 00:00:00 2001
From: filliatr
Date: Thu, 10 May 2001 15:02:00 +0000
Subject: message 'is defined' seulement en mode verbose

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1741 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/correctness/penv.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/contrib/correctness/penv.ml b/contrib/correctness/penv.ml
index 8604968e20..466905962d 100644
--- a/contrib/correctness/penv.ml
+++ b/contrib/correctness/penv.ml
@@ -221,7 +221,8 @@ let register id id' =
   try
     let (v,p) = Idmap.find id !edited in
     let _ = add_global id' v (Some p) in
-    mSGNL (hOV 0 [< 'sTR"Program "; pr_id id'; 'sPC; 'sTR"is defined" >]);
+    Options.if_verbose 
+      mSGNL (hOV 0 [< 'sTR"Program "; pr_id id'; 'sPC; 'sTR"is defined" >]);
     edited := Idmap.remove id !edited
   with Not_found -> ()
 
-- 
cgit v1.2.3