diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-04 17:07:21 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-04 17:07:21 +0000 |
| commit | 12f77536d29e6b6eeb2f1d065a805d353d197de9 (patch) | |
| tree | 705808fb7fb42f164530080fca762e0948d8b9e1 /parsing | |
| parent | 202903df7be549bea83735e9182814a7741e7f0d (diff) | |
Added a color output to Coqtop.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15421 85f007b7-540e-0410-9357-904b9bb8a0f7
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 -> |