diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index df42d9084..0df15babd 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -125,13 +125,13 @@ END let test_plural_form = function | [(_,([_],_))] -> - Flags.if_verbose msg_warning + Flags.if_verbose Feedback.msg_warning (strbrk "Keywords Variables/Hypotheses/Parameters expect more than one assumption") | _ -> () let test_plural_form_types = function | [([_],_)] -> - Flags.if_verbose msg_warning + Flags.if_verbose Feedback.msg_warning (strbrk "Keywords Implicit Types expect more than one type") | _ -> () @@ -448,7 +448,7 @@ GEXTEND Gram VernacInclude(e::l) | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type -> Flags.if_verbose - msg_warning (strbrk "Include Type is deprecated; use Include instead"); + Feedback.msg_warning (strbrk "Include Type is deprecated; use Include instead"); VernacInclude(e::l) ] ] ; export_token: @@ -667,7 +667,7 @@ 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 ]; "]" -> - msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead"); + Feedback. msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead"); VernacArgumentsScope (qid,scl) (* Implicit *) @@ -675,7 +675,7 @@ GEXTEND Gram pos = LIST0 [ "["; l = LIST0 implicit_name; "]" -> List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> Flags.if_verbose - msg_warning (strbrk "Implicit Arguments is deprecated; use Arguments instead"); + Feedback.msg_warning (strbrk "Implicit Arguments is deprecated; use Arguments instead"); VernacDeclareImplicits (qid,pos) | IDENT "Implicit"; "Type"; bl = reserv_list -> |