From bb76b246d1396f788d18888abe8284befb7f44b9 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 3 Apr 2001 08:04:19 +0000
Subject: utilisation de Options.if_verbose

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

(limited to 'proofs')

diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index c422b00699..b5f4d88f02 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -1189,5 +1189,5 @@ let add_tacdef na vbody =
          "There is already a Meta Definition or a Tactic Definition named ";
          'sTR na>];
     let _ = Lib.add_leaf (id_of_string na) OBJ (inMD (na,vbody)) in
-    if Options.is_verbose() then mSGNL [< 'sTR (na ^ " is defined") >]
+    Options.if_verbose mSGNL [< 'sTR (na ^ " is defined") >]
   end
-- 
cgit v1.2.3