Merge PR #8515: Command driven attributes

19 files changed, 161 insertions, 167 deletions

diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index c41687e721..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 Vernacinterp in
+| #[ locality; ] [ "Set" "Firstorder" "Solver" tactic(t) ] -> {
       set_default_solver
-        (Locality.make_section_locality atts.locality)
+        (Locality.make_section_locality locality)
         (Tacintern.glob_tactic t)
   }
 END
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index d4e410bd69..651895aa08 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1004,7 +1004,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
       Ensures by: obvious
       i*)
     (mk_equation_id f_id)
-    (Decl_kinds.Global, Flags.is_universe_polymorphism (), (Decl_kinds.Proof Decl_kinds.Theorem))
+    (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
     evd
   lemma_type
   (Lemmas.mk_hook (fun _ _ -> ()));
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index d57b931785..d1e7d8a5a8 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -307,7 +307,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   begin
     Lemmas.start_proof
       new_princ_name
-      (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem))
+      (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
       !evd
       (EConstr.of_constr new_principle_type)
       hook
@@ -359,10 +359,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
         let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
         let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
         (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
-        let univs =
-          let poly = Flags.is_universe_polymorphism () in
-          Evd.const_univ_entry ~poly evd'
-        in
+        let univs = Evd.const_univ_entry ~poly:false evd' in
         let ce = Declare.definition_entry ~univs value in
         ignore(
 	  Declare.declare_constant
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 7c80b776a4..98aaa081c3 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1494,7 +1494,7 @@ let do_build_inductive
   let _time2 = System.get_time () in
   try
     with_full_print
-      (Flags.silently (ComInductive.do_mutual_inductive ~template:None None rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters))
+      (Flags.silently (ComInductive.do_mutual_inductive ~template:None None rel_inds false false false ~uniform:ComInductive.NonUniformParameters))
       Declarations.Finite
   with
     | UserError(s,msg) as e ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 9a6169d42a..35acbea488 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -414,7 +414,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
       ComDefinition.do_definition
         ~program_mode:false
 	fname
-	(Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl
+        (Decl_kinds.Global,false,Decl_kinds.Definition) pl
 	bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()));
        let evd,rev_pconstants =
 	 List.fold_left
@@ -431,7 +431,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        in
        evd,List.rev rev_pconstants
     | _ ->
-       ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
+       ComFixpoint.do_fixpoint Global false fixpoint_exprl;
        let evd,rev_pconstants =
 	 List.fold_left
            (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 96eb7fbc60..d1a227d517 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -804,7 +804,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
 	 let (typ,_) = lemmas_types_infos.(i) in 
 	 Lemmas.start_proof
 	   lem_id
-	   (Decl_kinds.Global,Flags.is_universe_polymorphism (),((Decl_kinds.Proof Decl_kinds.Theorem)))
+           (Decl_kinds.Global,false,((Decl_kinds.Proof Decl_kinds.Theorem)))
            !evd
 	   typ
            (Lemmas.mk_hook (fun _ _ -> ()));
@@ -866,7 +866,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
 	   i*)
 	 let lem_id = mk_complete_id f_id in
 	 Lemmas.start_proof lem_id
-	   (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma
+           (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) sigma
 	 (fst lemmas_types_infos.(i))
            (Lemmas.mk_hook (fun _ _ -> ()));
 	 ignore (Pfedit.by
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 05a65e4cd8..85fb0c73c9 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -30,7 +30,7 @@ open Namegen
 open Tactypes
 open Tactics
 open Proofview.Notations
-open Vernacinterp
+open Attributes
 
 let wit_hyp = wit_var
 
@@ -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:atts.polymorphic 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:atts.polymorphic bl o (Some t) l }
-| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
-  { add_rewrite_hint ~poly:atts.polymorphic ["core"] o None l }
-| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
-  { add_rewrite_hint ~poly:atts.polymorphic ["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,45 +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 }
   -> {
-      let open Vernacinterp in
-      add_inversion_lemma_exn ~poly:atts.polymorphic 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 }
   -> {
-      let open Vernacinterp in
-      add_inversion_lemma_exn ~poly:atts.polymorphic 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 }
   -> {
-      let open Vernacinterp in
-      add_inversion_lemma_exn ~poly:atts.polymorphic 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 }
   -> {
-      let open Vernacinterp in
-      add_inversion_lemma_exn ~poly:atts.polymorphic 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 }
   -> {
-      let open Vernacinterp in
-      add_inversion_lemma_exn ~poly:atts.polymorphic 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 }
   -> {
-      let open Vernacinterp in
-      add_inversion_lemma_exn ~poly:atts.polymorphic 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 c07b653f3a..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 Vernacinterp 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 atts.locality)
+        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 d62f985350..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,12 +499,12 @@ 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 open Vernacinterp in
-      let n = Option.default 0 n in
-      let deprecation = atts.deprecated in
-      Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n ?deprecation r e;
+  {
+    let n = Option.default 0 n in
+    Tacentries.add_tactic_notation (Locality.make_module_locality locality) n ?deprecation r e;
   }
 END
 
@@ -545,13 +546,12 @@ 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 open Vernacinterp in
-           let deprecation = atts.deprecated in
-           Tacentries.register_ltac (Locality.make_module_locality atts.locality) ?deprecation l;
+  } -> {
+         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 26f2b08d3a..aa78fb5d1e 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -131,10 +131,9 @@ VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF
 END
 
 VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF
-| [ "Obligation" "Tactic" ":=" tactic(t) ] -> {
-        let open Vernacinterp in
+| #[ locality = Attributes.locality; ] [ "Obligation" "Tactic" ":=" tactic(t) ] -> {
         set_default_tactic
-          (Locality.make_section_locality atts.locality)
+          (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 3e47724c4c..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 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 a aeq n (Some lemma1) None None }
-  | [ "Add" "Relation" constr(a) constr(aeq)  "as" ident(n) ] ->
-      { declare_relation 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 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 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 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 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 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 ~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 ~binders:b a aeq n (Some lemma1) None None }
-  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)  "as" ident(n) ] ->
-      { declare_relation ~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 ~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 ~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 ~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 ~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 ~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) ] ->
-     { let open Vernacinterp in
-         add_setoid (not (Locality.make_section_locality atts.locality)) [] a aeq t n;
+  | #[ atts = rewrite_attributes; ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+     {
+         add_setoid atts [] a aeq t n;
      }
-  | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
-     { let open Vernacinterp in
-         add_setoid (not (Locality.make_section_locality atts.locality)) binders a aeq t n;
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(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 }
-    -> { let open Vernacinterp in
-           add_morphism_infer (not (Locality.make_section_locality atts.locality)) 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) }
-    -> { let open Vernacinterp in
-           add_morphism (not (Locality.make_section_locality atts.locality)) [] 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) }
-    -> { let open Vernacinterp in
-           add_morphism (not (Locality.make_section_locality atts.locality)) binders m s n;
+    -> {
+           add_morphism atts binders m s n;
        }
 END
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 8b2721ae4e..7d917c58fe 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -43,6 +43,14 @@ module NamedDecl = Context.Named.Declaration
 
 (** Typeclass-based generalized rewriting. *)
 
+type rewrite_attributes = { polymorphic : bool; program : bool; global : bool }
+
+let rewrite_attributes =
+  let open Attributes.Notations in
+  Attributes.(polymorphic ++ program ++ locality) >>= fun ((polymorphic, program), locality) ->
+  let global = not (Locality.make_section_locality locality) in
+  Attributes.Notations.return { polymorphic; program; global }
+
 (** Constants used by the tactic. *)
 
 let classes_dirpath =
@@ -1776,67 +1784,65 @@ let declare_an_instance n s args =
 
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
-let anew_instance global binders instance fields =
-  let program_mode = Flags.is_program_mode () in
-  let poly = Flags.is_universe_polymorphism () in
-  new_instance ~program_mode poly
+let anew_instance atts binders instance fields =
+  let program_mode = atts.program in
+  new_instance ~program_mode atts.polymorphic
     binders instance (Some (true, CAst.make @@ CRecord (fields)))
-    ~global ~generalize:false ~refine:false Hints.empty_hint_info
+    ~global:atts.global ~generalize:false ~refine:false Hints.empty_hint_info
 
-let declare_instance_refl global binders a aeq n lemma =
+let declare_instance_refl atts binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
-  in anew_instance global binders instance
+  in anew_instance atts binders instance
        [(qualid_of_ident (Id.of_string "reflexivity"),lemma)]
 
-let declare_instance_sym global binders a aeq n lemma =
+let declare_instance_sym atts binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric"
-  in anew_instance global binders instance
+  in anew_instance atts binders instance
        [(qualid_of_ident (Id.of_string "symmetry"),lemma)]
 
-let declare_instance_trans global binders a aeq n lemma =
+let declare_instance_trans atts binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive"
-  in anew_instance global binders instance
+  in anew_instance atts binders instance
        [(qualid_of_ident (Id.of_string "transitivity"),lemma)]
 
-let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
+let declare_relation atts ?(binders=[]) a aeq n refl symm trans =
   init_setoid ();
-  let global = not (Locality.make_section_locality locality) in
   let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation"
-  in ignore(anew_instance global binders instance []);
+  in ignore(anew_instance atts binders instance []);
   match (refl,symm,trans) with
       (None, None, None) -> ()
     | (Some lemma1, None, None) ->
-	ignore (declare_instance_refl global binders a aeq n lemma1)
+        ignore (declare_instance_refl atts binders a aeq n lemma1)
     | (None, Some lemma2, None) ->
-	ignore (declare_instance_sym global binders a aeq n lemma2)
+        ignore (declare_instance_sym atts binders a aeq n lemma2)
     | (None, None, Some lemma3) ->
-	ignore (declare_instance_trans global binders a aeq n lemma3)
+        ignore (declare_instance_trans atts binders a aeq n lemma3)
     | (Some lemma1, Some lemma2, None) ->
-	ignore (declare_instance_refl global binders a aeq n lemma1);
-	ignore (declare_instance_sym global binders a aeq n lemma2)
+        ignore (declare_instance_refl atts binders a aeq n lemma1);
+        ignore (declare_instance_sym atts binders a aeq n lemma2)
     | (Some lemma1, None, Some lemma3) ->
-	let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in
-	let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
+        let _lemma_refl = declare_instance_refl atts binders a aeq n lemma1 in
+        let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder"
 	in ignore(
-	    anew_instance global binders instance
+            anew_instance atts binders instance
               [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1);
                (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)])
     | (None, Some lemma2, Some lemma3) ->
-	let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
-	let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
+        let _lemma_sym = declare_instance_sym atts binders a aeq n lemma2 in
+        let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER"
 	in ignore(
-	    anew_instance global binders instance
+            anew_instance atts binders instance
               [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2);
                (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)])
      | (Some lemma1, Some lemma2, Some lemma3) ->
-	let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in
-	let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
-	let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
+        let _lemma_refl = declare_instance_refl atts binders a aeq n lemma1 in
+        let _lemma_sym = declare_instance_sym atts binders a aeq n lemma2 in
+        let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
 	in ignore(
-	  anew_instance global binders instance
+          anew_instance atts binders instance
             [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1);
              (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2);
              (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)])
@@ -1935,15 +1941,15 @@ let warn_add_setoid_deprecated =
   CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () ->
       Pp.(str "Add Setoid is deprecated, please use Add Parametric Relation."))
 
-let add_setoid global binders a aeq t n =
+let add_setoid atts binders a aeq t n =
   warn_add_setoid_deprecated ?loc:a.CAst.loc ();
   init_setoid ();
-  let _lemma_refl = declare_instance_refl global binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
-  let _lemma_sym = declare_instance_sym global binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
-  let _lemma_trans = declare_instance_trans global binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
+  let _lemma_refl = declare_instance_refl atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
+  let _lemma_sym = declare_instance_sym atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
+  let _lemma_trans = declare_instance_trans atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
   let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
   in ignore(
-    anew_instance global binders instance
+    anew_instance atts binders instance
       [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
        (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
        (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
@@ -1958,26 +1964,26 @@ let warn_add_morphism_deprecated =
   CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
       Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id"))
 
-let add_morphism_infer glob m n =
+let add_morphism_infer atts m n =
   warn_add_morphism_deprecated ?loc:m.CAst.loc ();
   init_setoid ();
-  let poly = Flags.is_universe_polymorphism () in
+  (* NB: atts.program is ignored, program mode automatically set by vernacentries *)
   let instance_id = add_suffix n "_Proper" in
   let env = Global.env () in
   let evd = Evd.from_env env in
   let uctx, instance = build_morphism_signature env evd m in
     if Lib.is_modtype () then
-      let uctx = UState.const_univ_entry ~poly uctx in
+      let uctx = UState.const_univ_entry ~poly:atts.polymorphic uctx in
       let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
 				(Entries.ParameterEntry 
                                  (None,(instance,uctx),None),
 				 Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
 	add_instance (Typeclasses.new_instance 
-                        (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob (ConstRef cst));
+                        (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst));
 	declare_projection n instance_id (ConstRef cst)
     else
-      let kind = Decl_kinds.Global, poly, 
+      let kind = Decl_kinds.Global, atts.polymorphic,
 	Decl_kinds.DefinitionBody Decl_kinds.Instance 
       in
       let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
@@ -1985,7 +1991,7 @@ let add_morphism_infer glob m n =
 	| Globnames.ConstRef cst ->
 	  add_instance (Typeclasses.new_instance 
 			  (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
-                          glob (ConstRef cst));
+                          atts.global (ConstRef cst));
 	  declare_projection n instance_id (ConstRef cst)
 	| _ -> assert false
       in
@@ -1995,9 +2001,8 @@ let add_morphism_infer glob m n =
 	    Lemmas.start_proof instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) hook;
 	    ignore (Pfedit.by (Tacinterp.interp tac))) ()
 
-let add_morphism glob binders m s n =
+let add_morphism atts binders m s n =
   init_setoid ();
-  let poly = Flags.is_universe_polymorphism () in
   let instance_id = add_suffix n "_Proper" in
   let instance =
     (((CAst.make @@ Name instance_id),None), Explicit,
@@ -2006,8 +2011,7 @@ let add_morphism glob binders m s n =
 	     [cHole; s; m]))
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
-  let program_mode = Flags.is_program_mode () in
-  ignore(new_instance ~program_mode ~global:glob poly binders instance
+  ignore(new_instance ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance
            (Some (true, CAst.make @@ CRecord []))
     ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
 
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 0d014a0bf3..4f46e78c71 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -19,6 +19,9 @@ open Tacinterp
 
 (** TODO: document and clean me! *)
 
+type rewrite_attributes
+val rewrite_attributes : rewrite_attributes Attributes.attribute
+
 type unary_strategy = 
     Subterms | Subterm | Innermost | Outermost
   | Bottomup | Topdown | Progress | Try | Any | Repeat
@@ -77,18 +80,18 @@ val cl_rewrite_clause :
 val is_applied_rewrite_relation :
   env -> evar_map -> rel_context -> constr -> types option
 
-val declare_relation : ?locality:bool ->
+val declare_relation : rewrite_attributes ->
   ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t ->
   constr_expr option -> constr_expr option -> constr_expr option -> unit
 
 val add_setoid :
-  bool -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr ->
+  rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr ->
   Id.t -> unit
 
-val add_morphism_infer : bool -> constr_expr -> Id.t -> unit
+val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> unit
 
 val add_morphism :
-  bool -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit
+  rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit
 
 val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
 
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 5b4bedb50a..c93d6251e0 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -12,7 +12,7 @@
 
 open Vernacexpr
 open Tacexpr
-open Vernacinterp
+open Attributes
 
 (** {5 Tactic Definitions} *)
 
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index a88285c9ee..d5f22b2c72 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -55,7 +55,7 @@ type alias = KerName.t
 type alias_tactic =
   { alias_args: Id.t list;
     alias_body: glob_tactic_expr;
-    alias_deprecation: Vernacinterp.deprecation option;
+    alias_deprecation: Attributes.deprecation option;
   }
 
 let alias_map = Summary.ref ~name:"tactic-alias"
@@ -121,7 +121,7 @@ type ltac_entry = {
   tac_for_ml : bool;
   tac_body : glob_tactic_expr;
   tac_redef : ModPath.t list;
-  tac_deprecation : Vernacinterp.deprecation option
+  tac_deprecation : Attributes.deprecation option
 }
 
 let mactab =
@@ -178,7 +178,7 @@ let subst_md (subst, (local, id, b, t, deprecation)) =
 let classify_md (local, _, _, _, _ as o) = Substitute o
 
 let inMD : bool * ltac_constant option * bool * glob_tactic_expr *
-           Vernacinterp.deprecation option -> obj =
+           Attributes.deprecation option -> obj =
   declare_object {(default_object "TAC-DEFINITION") with
      cache_function  = cache_md;
      load_function   = load_md;
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index d5d36c97fa..5b98daf383 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -12,7 +12,7 @@ open Names
 open Libnames
 open Tacexpr
 open Geninterp
-open Vernacinterp
+open Attributes
 
 (** This module centralizes the various ways of registering tactics. *)
 
@@ -33,7 +33,7 @@ type alias = KerName.t
 type alias_tactic =
   { alias_args: Id.t list;
     alias_body: glob_tactic_expr;
-    alias_deprecation: Vernacinterp.deprecation option;
+    alias_deprecation: deprecation option;
   }
 (** Contents of a tactic notation *)
 
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 5e2a9af7e5..ebec3c887c 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -122,15 +122,15 @@ let warn_deprecated_tactic =
   CWarnings.create ~name:"deprecated-tactic" ~category:"deprecated"
     (fun (qid,depr) -> str "Tactic " ++ pr_qualid qid ++
       strbrk " is deprecated" ++
-      pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++
-      str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note)
+      pr_opt (fun since -> str "since " ++ str since) depr.Attributes.since ++
+      str "." ++ pr_opt (fun note -> str note) depr.Attributes.note)
 
 let warn_deprecated_alias =
   CWarnings.create ~name:"deprecated-tactic-notation" ~category:"deprecated"
     (fun (kn,depr) -> str "Tactic Notation " ++ Pptactic.pr_alias_key kn ++
       strbrk " is deprecated since" ++
-      pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++
-      str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note)
+      pr_opt (fun since -> str "since " ++ str since) depr.Attributes.since ++
+      str "." ++ pr_opt (fun note -> str note) depr.Attributes.note)
 
 let intern_isolated_global_tactic_reference qid =
   let loc = qid.CAst.loc in
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 940defb743..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 Vernacinterp in
-         let locality = Locality.make_section_locality atts.locality 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 5dbc9eea7a..13e0bcbd47 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -16,7 +16,6 @@ open Notation
 open Numeral
 open Pp
 open Names
-open Vernacinterp
 open Ltac_plugin
 open Stdarg
 open Pcoq.Prim
@@ -36,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 atts.locality) 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