diff options
Diffstat (limited to 'parsing')
| -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 3263de8d5..445908fba 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -136,13 +136,13 @@ END let test_plurial_form = function | [(_,([_],_))] -> Flags.if_verbose msg_warning - (str "Keywords Variables/Hypotheses/Parameters expect more than one assumption") + (strbrk "Keywords Variables/Hypotheses/Parameters expect more than one assumption") | _ -> () let test_plurial_form_types = function | [([_],_)] -> Flags.if_verbose msg_warning - (str "Keywords Implicit Types expect more than one type") + (strbrk "Keywords Implicit Types expect more than one type") | _ -> () (* Gallina declarations *) @@ -423,7 +423,7 @@ GEXTEND Gram VernacInclude(e::l) | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type -> Flags.if_verbose - msg_warning (str "Include Type is deprecated; use Include instead"); + msg_warning (strbrk "Include Type is deprecated; use Include instead"); VernacInclude(e::l) ] ] ; export_token: @@ -629,7 +629,7 @@ GEXTEND Gram | IDENT "Arguments"; IDENT "Scope"; qid = smart_global; "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" -> Flags.if_verbose - msg_warning (str "Arguments Scope is deprecated; use Arguments instead"); + msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead"); VernacArgumentsScope (use_section_locality (),qid,scl) (* Implicit *) @@ -637,7 +637,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 (str "Implicit Arguments is deprecated; use Arguments instead"); + msg_warning (strbrk "Implicit Arguments is deprecated; use Arguments instead"); VernacDeclareImplicits (use_section_locality (),qid,pos) | IDENT "Implicit"; "Type"; bl = reserv_list -> |