diff options
| author | ppedrot | 2013-05-08 19:55:23 +0000 |
|---|---|---|
| committer | ppedrot | 2013-05-08 19:55:23 +0000 |
| commit | d63320ceb1c56710f5e953742dd5d6cf43aacbdf (patch) | |
| tree | 9a6eec0f6e330270aab09af8ae9c744282dc8a82 /interp/notation.ml | |
| parent | c9467e5684f9a71cb82ddc72b5b9d501b32b5c5e (diff) | |
Uniformizing the [if_warn] flag used for warning printing and put
it into the standard logger instead.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16491 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index d0b4651ec3..9bbaf9d867 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -182,7 +182,7 @@ let declare_delimiters scope key = | None -> scope_map := Gmap.add scope newsc !scope_map | Some oldkey when String.equal oldkey key -> () | Some oldkey -> - Flags.if_warn msg_warning + msg_warning (strbrk ("Overwriting previous delimiting key "^oldkey^" in scope "^scope)); scope_map := Gmap.add scope newsc !scope_map end; @@ -190,7 +190,7 @@ let declare_delimiters scope key = let oldscope = Gmap.find key !delimiters_map in if String.equal oldscope scope then () else begin - Flags.if_warn msg_warning (strbrk ("Hiding binding of key "^key^" to "^oldscope)); + msg_warning (strbrk ("Hiding binding of key "^key^" to "^oldscope)); delimiters_map := Gmap.add key scope !delimiters_map end with Not_found -> delimiters_map := Gmap.add key scope !delimiters_map @@ -353,7 +353,7 @@ let declare_notation_interpretation ntn scopt pat df = | None -> "" | Some _ -> " in scope " ^ scope in let message = "Notation " ^ ntn ^ " was already used" ^ which_scope in - Flags.if_warn msg_warning (strbrk message) + msg_warning (strbrk message) in let sc = { sc with notations = Gmap.add ntn (pat,df) sc.notations } in let () = scope_map := Gmap.add scope sc !scope_map in |