diff options
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/tacextend.ml4 | 6 | ||||
| -rw-r--r-- | grammar/vernacextend.ml4 | 6 |
2 files changed, 6 insertions, 6 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 3a47ade0df..06c3ac3f94 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -54,9 +54,9 @@ let rec extract_signature = function let check_unicity s l = let l' = List.map (fun (l,_) -> extract_signature l) l in if not (Util.list_distinct l') then - Pp.warning_with !Pp_control.err_ft - ("Two distinct rules of tactic entry "^s^" have the same\n"^ - "non-terminals in the same order: put them in distinct tactic entries") + Pp.msg_warning + (strbrk ("Two distinct rules of tactic entry "^s^" have the same "^ + "non-terminals in the same order: put them in distinct tactic entries")) let make_clause (pt,e) = (make_patt pt, diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index af7ee7d169..b66460fe6f 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -31,9 +31,9 @@ let rec make_let e = function let check_unicity s l = let l' = List.map (fun (_,l,_) -> extract_signature l) l in if not (Util.list_distinct l') then - Pp.warning_with !Pp_control.err_ft - ("Two distinct rules of entry "^s^" have the same\n"^ - "non-terminals in the same order: put them in distinct vernac entries") + Pp.msg_warning + (strbrk ("Two distinct rules of entry "^s^" have the same "^ + "non-terminals in the same order: put them in distinct vernac entries")) let make_clause (_,pt,e) = (make_patt pt, |