diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 54 |
1 files changed, 33 insertions, 21 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index f0475ee25..7184136e8 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -123,16 +123,18 @@ GEXTEND Gram ; END -let test_plural_form = function +let warn_plural_command = + CWarnings.create ~name:"plural-command" ~category:"pedantic" ~default:CWarnings.Disabled + (fun kwd -> strbrk (Printf.sprintf "Command \"%s\" expects more than one assumption." kwd)) + +let test_plural_form loc kwd = function | [(_,([_],_))] -> - Flags.if_verbose Feedback.msg_warning - (strbrk "Keywords Variables/Hypotheses/Parameters expect more than one assumption") + warn_plural_command ~loc:!@loc kwd | _ -> () -let test_plural_form_types = function +let test_plural_form_types loc kwd = function | [([_],_)] -> - Flags.if_verbose Feedback.msg_warning - (strbrk "Keywords Implicit Types expect more than one type") + warn_plural_command ~loc:!@loc kwd | _ -> () let fresh_var env c = @@ -155,8 +157,8 @@ GEXTEND Gram VernacStartTheoremProof (thm, (Some id,(bl,c,None))::l, false) | stre = assumption_token; nl = inline; bl = assum_list -> VernacAssumption (stre, nl, bl) - | stre = assumptions_token; nl = inline; bl = assum_list -> - test_plural_form bl; + | (kwd,stre) = assumptions_token; nl = inline; bl = assum_list -> + test_plural_form loc kwd bl; VernacAssumption (stre, nl, bl) | d = def_token; id = pidentref; b = def_body -> VernacDefinition (d, id, b) @@ -209,11 +211,11 @@ GEXTEND Gram | IDENT "Conjecture" -> (None, Conjectural) ] ] ; assumptions_token: - [ [ IDENT "Hypotheses" -> (Some Discharge, Logical) - | IDENT "Variables" -> (Some Discharge, Definitional) - | IDENT "Axioms" -> (None, Logical) - | IDENT "Parameters" -> (None, Definitional) - | IDENT "Conjectures" -> (None, Conjectural) ] ] + [ [ kwd = IDENT "Hypotheses" -> (kwd, (Some Discharge, Logical)) + | kwd = IDENT "Variables" -> (kwd, (Some Discharge, Definitional)) + | kwd = IDENT "Axioms" -> (kwd, (None, Logical)) + | kwd = IDENT "Parameters" -> (kwd, (None, Definitional)) + | kwd = IDENT "Conjectures" -> (kwd, (None, Conjectural)) ] ] ; inline: [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i) @@ -422,6 +424,10 @@ let starredidentreflist_to_expr l = | [] -> SsEmpty | x :: xs -> List.fold_right (fun i acc -> SsUnion(i,acc)) xs x +let warn_deprecated_include_type = + CWarnings.create ~name:"deprecated-include-type" ~category:"deprecated" + (fun () -> strbrk "Include Type is deprecated; use Include instead") + (* Modules and Sections *) GEXTEND Gram GLOBAL: gallina_ext module_expr module_type section_subset_expr; @@ -461,9 +467,8 @@ GEXTEND Gram | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr -> VernacInclude(e::l) | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type -> - Flags.if_verbose - Feedback.msg_warning (strbrk "Include Type is deprecated; use Include instead"); - VernacInclude(e::l) ] ] + warn_deprecated_include_type ~loc:!@loc (); + VernacInclude(e::l) ] ] ; export_token: [ [ IDENT "Import" -> Some false @@ -567,6 +572,14 @@ GEXTEND Gram ; END +let warn_deprecated_arguments_scope = + CWarnings.create ~name:"deprecated-arguments-scope" ~category:"deprecated" + (fun () -> strbrk "Arguments Scope is deprecated; use Arguments instead") + +let warn_deprecated_implicit_arguments = + CWarnings.create ~name:"deprecated-implicit-arguments" ~category:"deprecated" + (fun () -> strbrk "Implicit Arguments is deprecated; use Arguments instead") + (* Extensions: implicits, coercions, etc. *) GEXTEND Gram GLOBAL: gallina_ext instance_name; @@ -681,22 +694,21 @@ 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 ]; "]" -> - Feedback. msg_warning (strbrk "Arguments Scope is deprecated; use Arguments instead"); + warn_deprecated_arguments_scope ~loc:!@loc (); VernacArgumentsScope (qid,scl) (* Implicit *) | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global; pos = LIST0 [ "["; l = LIST0 implicit_name; "]" -> List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> - Flags.if_verbose - Feedback.msg_warning (strbrk "Implicit Arguments is deprecated; use Arguments instead"); - VernacDeclareImplicits (qid,pos) + warn_deprecated_implicit_arguments ~loc:!@loc (); + VernacDeclareImplicits (qid,pos) | IDENT "Implicit"; "Type"; bl = reserv_list -> VernacReserve bl | IDENT "Implicit"; IDENT "Types"; bl = reserv_list -> - test_plural_form_types bl; + test_plural_form_types loc "Implicit Types" bl; VernacReserve bl | IDENT "Generalizable"; |