diff options
| author | herbelin | 2007-02-24 15:22:07 +0000 |
|---|---|---|
| committer | herbelin | 2007-02-24 15:22:07 +0000 |
| commit | f7a82d5f7edcce7ef70b99a10b92d8dcd5cfea70 (patch) | |
| tree | 7248e936a9094bff92ed96e666c8feb1941b5802 /interp/notation.ml | |
| parent | 8eeec81e418603eaffc295bf20744da91b2e0f83 (diff) | |
Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbose +
ajout Pp.strbrk pour faciliter les césures faciles + messages divers).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9679 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 3989f00727..614c87a0cf 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -299,8 +299,8 @@ let level_of_notation ntn = let declare_notation_interpretation ntn scopt pat df = let scope = match scopt with Some s -> s | None -> default_scope in let sc = find_scope scope in - if Gmap.mem ntn sc.notations && Options.is_verbose () then - msg_warning (str ("Notation "^ntn^" was already used"^ + if Gmap.mem ntn sc.notations then + Options.if_warn msg_warning (str ("Notation "^ntn^" was already used"^ (if scopt = None then "" else " in scope "^scope))); let sc = { sc with notations = Gmap.add ntn (pat,df) sc.notations } in scope_map := Gmap.add scope sc !scope_map; |