diff options
| author | ppedrot | 2012-06-01 20:08:33 +0000 |
|---|---|---|
| committer | ppedrot | 2012-06-01 20:08:33 +0000 |
| commit | a92a0d051b987ba996905ccd4ce7ee3a5feb41c1 (patch) | |
| tree | ec5246ac1cfc741dc30c33fe6551216dfdef6a54 /grammar | |
| parent | 80b91aa1e83097efd006cfed5f57e4826a1ab0c8 (diff) | |
More cleaning
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15414 85f007b7-540e-0410-9357-904b9bb8a0f7
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, |