aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--toplevel/metasyntax.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 905df5f2bc..09d4bff43b 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -686,7 +686,7 @@ let is_not_small_constr = function
let rec define_keywords_aux = function
| GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l
when is_not_small_constr e ->
- msg_info (strbrk ("Identifier '"^k^"' now a keyword"));
+ Flags.if_verbose msg_info (strbrk ("Identifier '"^k^"' now a keyword"));
Lexer.add_keyword k;
n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
| n :: l -> n :: define_keywords_aux l
@@ -695,7 +695,7 @@ let rec define_keywords_aux = function
(* Ensure that IDENT articulation terminal symbols are keywords *)
let define_keywords = function
| GramConstrTerminal(IDENT k)::l ->
- msg_info (strbrk ("Identifier '"^k^"' now a keyword"));
+ Flags.if_verbose msg_info (strbrk ("Identifier '"^k^"' now a keyword"));
Lexer.add_keyword k;
GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
| l -> define_keywords_aux l