From 0a478031f0213ef74c3649ea1a8d58aa89e54416 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 16 Oct 2018 14:42:53 +0200 Subject: coqpp VERNAC EXTEND uses #[ att = attribute; ] syntax I think for instance the new code in this diff is cleaner and more systematic: ~~~diff VERNAC COMMAND EXTEND VernacDeclareTacticDefinition -| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => { +| #[ deprecation; locality; ] [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => { VtSideff (List.map (function | TacticDefinition ({CAst.v=r},_) -> r | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater } -> { - let deprecation, locality = Attributes.(parse Notations.(deprecation ++ locality) atts) in Tacentries.register_ltac (Locality.make_module_locality locality) ?deprecation l; } END ~~~ --- coqpp/coqpp_ast.mli | 1 + coqpp/coqpp_lex.mll | 1 + coqpp/coqpp_main.ml | 47 ++++++++++++++++++++++- coqpp/coqpp_parse.mly | 29 +++++++++++--- plugins/firstorder/g_ground.mlg | 6 +-- plugins/ltac/extratactics.mlg | 40 ++++++++++---------- plugins/ltac/g_auto.mlg | 5 +-- plugins/ltac/g_ltac.mlg | 8 ++-- plugins/ltac/g_obligations.mlg | 4 +- plugins/ltac/g_rewrite.mlg | 84 ++++++++++++++++++++--------------------- plugins/ssr/ssrvernac.mlg | 5 +-- plugins/syntax/g_numeral.mlg | 4 +- 12 files changed, 147 insertions(+), 87 deletions(-) diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli index 93a07cff9d..8e10ec49ce 100644 --- a/coqpp/coqpp_ast.mli +++ b/coqpp/coqpp_ast.mli @@ -102,6 +102,7 @@ type classification = | ClassifName of string type vernac_rule = { + vernac_atts : (string * string) list option; vernac_toks : ext_token list; vernac_class : code option; vernac_depr : bool; diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll index cdea4b99ef..c38755943a 100644 --- a/coqpp/coqpp_lex.mll +++ b/coqpp/coqpp_lex.mll @@ -130,6 +130,7 @@ rule extend = parse | space { extend lexbuf } | '\"' { string lexbuf } | '\n' { newline lexbuf; extend lexbuf } +| "#[" { HASHBRACKET } | '[' { LBRACKET } | ']' { RBRACKET } | '|' { PIPE } diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 5314806c24..7cecff9d75 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -309,9 +309,52 @@ let print_rule_classifier fmt r = match r.vernac_class with else fprintf fmt "Some @[(fun %a-> %a)@]" print_binders r.vernac_toks print_code f +(* let print_atts fmt = function *) +(* | None -> fprintf fmt "@[let () = Attributes.unsupported_attributes atts in@] " *) +(* | Some atts -> *) +(* let rec print_left fmt = function *) +(* | [] -> assert false *) +(* | [x,_] -> fprintf fmt "%s" x *) +(* | (x,_) :: rem -> fprintf fmt "(%s, %a)" x print_left rem *) +(* in *) +(* let rec print_right fmt = function *) +(* | [] -> assert false *) +(* | [_,y] -> fprintf fmt "%s" y *) +(* | (_,y) :: rem -> fprintf fmt "(%s ++ %a)" y print_right rem *) +(* in *) +(* let nota = match atts with [_] -> "" | _ -> "Attributes.Notations." in *) +(* fprintf fmt "@[let %a = Attributes.parse %s(%a) atts in@] " *) +(* print_left atts nota print_right atts *) + +let print_atts_left fmt = function + | None -> fprintf fmt "()" + | Some atts -> + let rec aux fmt = function + | [] -> assert false + | [x,_] -> fprintf fmt "%s" x + | (x,_) :: rem -> fprintf fmt "(%s, %a)" x aux rem + in + aux fmt atts + +let print_atts_right fmt = function + | None -> fprintf fmt "(Attributes.unsupported_attributes atts)" + | Some atts -> + let rec aux fmt = function + | [] -> assert false + | [_,y] -> fprintf fmt "%s" y + | (_,y) :: rem -> fprintf fmt "(%s ++ %a)" y aux rem + in + let nota = match atts with [_] -> "" | _ -> "Attributes.Notations." in + fprintf fmt "(Attributes.parse %s%a atts)" nota aux atts + +let print_body_fun fmt r = + fprintf fmt "let coqpp_body %a%a ~st = let () = %a in st in " + print_binders r.vernac_toks print_atts_left r.vernac_atts print_code r.vernac_body + let print_body fmt r = - fprintf fmt "@[(fun %a~atts@ ~st@ -> let () = %a in st)@]" - print_binders r.vernac_toks print_code r.vernac_body + fprintf fmt "@[(%afun %a~atts@ ~st@ -> coqpp_body %a%a ~st)@]" + print_body_fun r print_binders r.vernac_toks + print_binders r.vernac_toks print_atts_right r.vernac_atts let rec print_sig fmt = function | [] -> fprintf fmt "@[Vernacentries.TyNil@]" diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly index 1fb5461b21..abe52ab46b 100644 --- a/coqpp/coqpp_parse.mly +++ b/coqpp/coqpp_parse.mly @@ -65,7 +65,7 @@ let parse_user_entry s sep = %token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED ARGUMENT %token RAW_PRINTED GLOB_PRINTED %token COMMAND CLASSIFIED PRINTED TYPED INTERPRETED GLOBALIZED SUBSTITUTED BY AS -%token LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL STAR +%token HASHBRACKET LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL STAR %token LPAREN RPAREN COLON SEMICOLON %token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA %token EOF @@ -209,15 +209,32 @@ vernac_rules: ; vernac_rule: -| PIPE LBRACKET ext_tokens RBRACKET rule_deprecation rule_classifier ARROW CODE +| PIPE vernac_attributes_opt LBRACKET ext_tokens RBRACKET rule_deprecation rule_classifier ARROW CODE { { - vernac_toks = $3; - vernac_depr = $5; - vernac_class= $6; - vernac_body = $8; + vernac_atts = $2; + vernac_toks = $4; + vernac_depr = $6; + vernac_class= $7; + vernac_body = $9; } } ; +vernac_attributes_opt: +| { None } +| HASHBRACKET vernac_attributes RBRACKET { Some $2 } +; + +vernac_attributes: +| vernac_attribute { [$1] } +| vernac_attribute SEMICOLON { [$1] } +| vernac_attribute SEMICOLON vernac_attributes { $1 :: $3 } +; + +vernac_attribute: +| qualid_or_ident EQUAL qualid_or_ident { ($1, $3) } +| qualid_or_ident { ($1, $1) } +; + rule_deprecation: | { false } | DEPRECATED { true } diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index 14a3acad57..b9274cf6b8 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -20,6 +20,7 @@ open Tacticals.New open Tacinterp open Stdarg open Tacarg +open Attributes open Pcoq.Prim } @@ -73,10 +74,9 @@ let (set_default_solver, default_solver, print_default_solver) = } VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF -| [ "Set" "Firstorder" "Solver" tactic(t) ] -> { - let open Attributes in +| #[ locality; ] [ "Set" "Firstorder" "Solver" tactic(t) ] -> { set_default_solver - (Locality.make_section_locality (only_locality atts)) + (Locality.make_section_locality locality) (Tacintern.glob_tactic t) } END diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index cab7281719..73ec94f75f 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -321,15 +321,15 @@ let classify_hint _ = Vernacexpr.VtSideff [], Vernacexpr.VtLater } VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY { classify_hint } -| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] -> - { add_rewrite_hint ~poly:(only_polymorphism atts) bl o None l } -| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) +| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] -> + { add_rewrite_hint ~poly:polymorphic bl o None l } +| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ":" preident_list(bl) ] -> - { add_rewrite_hint ~poly:(only_polymorphism atts) bl o (Some t) l } -| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] -> - { add_rewrite_hint ~poly:(only_polymorphism atts) ["core"] o None l } -| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] -> - { add_rewrite_hint ~poly:(only_polymorphism atts) ["core"] o (Some t) l } + { add_rewrite_hint ~poly:polymorphic bl o (Some t) l } +| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] -> + { add_rewrite_hint ~poly:polymorphic ["core"] o None l } +| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] -> + { add_rewrite_hint ~poly:polymorphic ["core"] o (Some t) l } END (**********************************************************************) @@ -411,39 +411,39 @@ let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater END*) VERNAC COMMAND EXTEND DeriveInversionClear -| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] +| #[ polymorphic; ] [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] => { seff na } -> { - add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c s false inv_clear_tac } + add_inversion_lemma_exn ~poly:polymorphic na c s false inv_clear_tac } -| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => { seff na } +| #[ polymorphic; ] [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => { seff na } -> { - add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c Sorts.InProp false inv_clear_tac } + add_inversion_lemma_exn ~poly:polymorphic na c Sorts.InProp false inv_clear_tac } END VERNAC COMMAND EXTEND DeriveInversion -| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] +| #[ polymorphic; ] [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] => { seff na } -> { - add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c s false inv_tac } + add_inversion_lemma_exn ~poly:polymorphic na c s false inv_tac } -| [ "Derive" "Inversion" ident(na) "with" constr(c) ] => { seff na } +| #[ polymorphic; ] [ "Derive" "Inversion" ident(na) "with" constr(c) ] => { seff na } -> { - add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c Sorts.InProp false inv_tac } + add_inversion_lemma_exn ~poly:polymorphic na c Sorts.InProp false inv_tac } END VERNAC COMMAND EXTEND DeriveDependentInversion -| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] +| #[ polymorphic; ] [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] => { seff na } -> { - add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c s true dinv_tac } + add_inversion_lemma_exn ~poly:polymorphic na c s true dinv_tac } END VERNAC COMMAND EXTEND DeriveDependentInversionClear -| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] +| #[ polymorphic; ] [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] => { seff na } -> { - add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c s true dinv_clear_tac } + add_inversion_lemma_exn ~poly:polymorphic na c s true dinv_clear_tac } END (**********************************************************************) diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index e8b5e900dd..5af393a3e5 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -239,10 +239,9 @@ ARGUMENT EXTEND opthints END VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF -| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> { - let open Attributes in +| #[ locality = Attributes.locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> { let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in - Hints.add_hints ~local:(Locality.make_section_locality (only_locality atts)) + Hints.add_hints ~local:(Locality.make_section_locality locality) (match dbnames with None -> ["core"] | Some l -> l) entry; } END diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index f8842b201c..c58c8556c5 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -22,6 +22,7 @@ open Genarg open Genredexpr open Tok (* necessary for camlp5 *) open Names +open Attributes open Pcoq open Pcoq.Prim @@ -498,11 +499,11 @@ VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY { pr_ltac_production_item END VERNAC COMMAND EXTEND VernacTacticNotation -| [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => +| #[ deprecation; locality; ] + [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => { VtSideff [], VtNow } -> { let n = Option.default 0 n in - let deprecation, locality = Attributes.(parse Notations.(deprecation ++ locality) atts) in Tacentries.add_tactic_notation (Locality.make_module_locality locality) n ?deprecation r e; } END @@ -545,12 +546,11 @@ PRINTED BY { pr_tacdef_body } END VERNAC COMMAND EXTEND VernacDeclareTacticDefinition -| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => { +| #[ deprecation; locality; ] [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => { VtSideff (List.map (function | TacticDefinition ({CAst.v=r},_) -> r | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater } -> { - let deprecation, locality = Attributes.(parse Notations.(deprecation ++ locality) atts) in Tacentries.register_ltac (Locality.make_module_locality locality) ?deprecation l; } END diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index 030b1b5410..aa78fb5d1e 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -131,9 +131,9 @@ VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF END VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF -| [ "Obligation" "Tactic" ":=" tactic(t) ] -> { +| #[ locality = Attributes.locality; ] [ "Obligation" "Tactic" ":=" tactic(t) ] -> { set_default_tactic - (Locality.make_section_locality (Attributes.only_locality atts)) + (Locality.make_section_locality locality) (Tacintern.glob_tactic t); } END diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 6a8368d863..1c7220ddc0 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -180,36 +180,36 @@ TACTIC EXTEND setoid_rewrite END VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF - | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> - { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n (Some lemma1) (Some lemma2) None } + { declare_relation atts a aeq n (Some lemma1) (Some lemma2) None } - | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "as" ident(n) ] -> - { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n (Some lemma1) None None } - | [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> - { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n None None None } + { declare_relation atts a aeq n (Some lemma1) None None } + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> + { declare_relation atts a aeq n None None None } END VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF - | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> - { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n None (Some lemma2) None } - | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n None (Some lemma2) (Some lemma3) } + { declare_relation atts a aeq n None (Some lemma2) None } + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + { declare_relation atts a aeq n None (Some lemma2) (Some lemma3) } END VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF - | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n (Some lemma1) None (Some lemma3) } - | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + { declare_relation atts a aeq n (Some lemma1) None (Some lemma3) } + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } - | [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + { declare_relation atts a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } + | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - { declare_relation (Attributes.parse rewrite_attributes atts) a aeq n None None (Some lemma3) } + { declare_relation atts a aeq n None None (Some lemma3) } END { @@ -236,64 +236,64 @@ GRAMMAR EXTEND Gram END VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> - { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n (Some lemma1) (Some lemma2) None } - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) + { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) None } + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "as" ident(n) ] -> - { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n (Some lemma1) None None } - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> - { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n None None None } + { declare_relation atts ~binders:b a aeq n (Some lemma1) None None } + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> + { declare_relation atts ~binders:b a aeq n None None None } END VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> - { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n None (Some lemma2) None } - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n None (Some lemma2) (Some lemma3) } + { declare_relation atts ~binders:b a aeq n None (Some lemma2) None } + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + { declare_relation atts ~binders:b a aeq n None (Some lemma2) (Some lemma3) } END VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n (Some lemma1) None (Some lemma3) } - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + { declare_relation atts ~binders:b a aeq n (Some lemma1) None (Some lemma3) } + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - { declare_relation (Attributes.parse rewrite_attributes atts) ~binders:b a aeq n None None (Some lemma3) } + { declare_relation atts ~binders:b a aeq n None None (Some lemma3) } END VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF - | [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> { - add_setoid (Attributes.parse rewrite_attributes atts) [] a aeq t n; + add_setoid atts [] a aeq t n; } - | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> { - add_setoid (Attributes.parse rewrite_attributes atts) binders a aeq t n; + add_setoid atts binders a aeq t n; } - | [ "Add" "Morphism" constr(m) ":" ident(n) ] + | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) ":" ident(n) ] (* This command may or may not open a goal *) => { Vernacexpr.VtUnknown, Vernacexpr.VtNow } -> { - add_morphism_infer (Attributes.parse rewrite_attributes atts) m n; + add_morphism_infer atts m n; } - | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] + | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) } -> { - add_morphism (Attributes.parse rewrite_attributes atts) [] m s n; + add_morphism atts [] m s n; } - | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) + | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) } -> { - add_morphism (Attributes.parse rewrite_attributes atts) binders m s n; + add_morphism atts binders m s n; } END diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 2774b843aa..4ed75cdbe4 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -170,10 +170,9 @@ let declare_one_prenex_implicit locality f = } VERNAC COMMAND EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF - | [ "Prenex" "Implicits" ne_global_list(fl) ] + | #[ locality = Attributes.locality; ] [ "Prenex" "Implicits" ne_global_list(fl) ] -> { - let open Attributes in - let locality = Locality.make_section_locality (only_locality atts) in + let locality = Locality.make_section_locality locality in List.iter (declare_one_prenex_implicit locality) fl; } END diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index e70edd56cb..13e0bcbd47 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -35,7 +35,7 @@ ARGUMENT EXTEND numnotoption END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF - | [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) numnotoption(o) ] -> - { vernac_numeral_notation (Locality.make_module_locality (Attributes.only_locality atts)) ty f g (Id.to_string sc) o } + { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } END -- cgit v1.2.3