From 3378c2cc6a403e78f3fd800dcaca67a82bfb9b4d Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 29 Jan 2001 16:09:36 +0000
Subject: pas de warning avec Opaque quand is_silent

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

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index e17490ddbd..e204b6d92c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -547,8 +547,9 @@ let _ =
 	 id_list)
 
 let warning_opaque s =
-  warning (
-    "This command turns the constants which depend on the definition/proof
+  if not(is_silent()) then 
+    warning
+      ("This command turns the constants which depend on the definition/proof
 of "^s^" un-re-checkable until the next \"Transparent "^s^"\" command.")
 
 let _ =
-- 
cgit v1.2.3