diff options
| -rw-r--r-- | parsing/g_vernac.ml4 | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 004dbab7b4..7a78a7dae2 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -622,9 +622,8 @@ GEXTEND Gram (* moved there so that camlp5 factors it with the previous rule *) | IDENT "Arguments"; IDENT "Scope"; qid = smart_global; "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" -> - Flags.if_verbose - msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead"); - VernacArgumentsScope (qid,scl) + msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead"); + VernacArgumentsScope (qid,scl) (* Implicit *) | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; |