diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-05-21 06:23:28 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-05-21 06:23:28 +0000 |
| commit | e63eec5fa9517d05036f4dbf3b86b2d81ab4a07b (patch) | |
| tree | 37ee43ce19f64d8fd3365a56ec4e0ab47feff9d7 | |
| parent | 9accb5a66da5d68fa01c4c3b8e7b74985e84f6fa (diff) | |
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
| -rw-r--r-- | pretyping/tacred.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index ef3869d27..fa62c4465 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) |