summaryrefslogtreecommitdiff
path: root/toplevel/metasyntax.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2014-01-19 15:09:26 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2014-01-19 15:09:26 +0100
commit58545b00a1c1825d9e51b16c2986976dd45dd3b2 (patch)
treec19584a3daef4f5cb042291f8079225e09e5e751 /toplevel/metasyntax.ml
parentbdb99a4e91d98fa7be517808945e7f1c96dd8003 (diff)
parentd2c5c5e616a6e118291fe1ce9965c731adac03a8 (diff)
Merge tag 'upstream/8.4pl3dfsg'
Upstream version 8.4pl3dfsg
Diffstat (limited to 'toplevel/metasyntax.ml')
-rw-r--r--toplevel/metasyntax.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 006dc5ec..7653bfc4 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -851,7 +851,7 @@ let check_rule_productivity l =
error "A recursive notation must start with at least one symbol."
let is_not_printable = function
- | AVar _ -> warning "This notation will not be used for printing as it is bound to a \nsingle variable"; true
+ | AVar _ -> msg_warn "This notation will not be used for printing as it is bound to a \nsingle variable"; true
| _ -> false
let find_precedence lev etyps symbols =
@@ -909,7 +909,7 @@ let remove_curly_brackets l =
(match next' with
| Terminal "}" as t2 :: l'' as l1 ->
if l <> l0 or l' <> l1 then
- warning "Skipping spaces inside curly brackets";
+ msg_warn "Skipping spaces inside curly brackets";
if deb & l'' = [] then [t1;x;t2] else begin
check_curly_brackets_notation_exists ();
x :: aux false l''