From e63eec5fa9517d05036f4dbf3b86b2d81ab4a07b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 21 May 2007 06:23:28 +0000
Subject: Protection d'un warning par if_verbose

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9843 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/tacred.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index ef3869d278..fa62c44657 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -744,10 +744,12 @@ let rec substlin env name n ol c =
                (n2,ol2,mkCast (c1',k,c2')))
 
     | Fix _ -> 
-        (warning "do not consider occurrences inside fixpoints"; (n,ol,c))
+        (Options.if_verbose
+	  warning "do not consider occurrences inside fixpoints"; (n,ol,c))
 	
     | CoFix _ -> 
-        (warning "do not consider occurrences inside cofixpoints"; (n,ol,c))
+        (Options.if_verbose
+	  warning "do not consider occurrences inside cofixpoints"; (n,ol,c))
 
     | (Rel _|Meta _|Var _|Sort _
       |Evar _|Const _|Ind _|Construct _) -> (n,ol,c)
-- 
cgit v1.2.3