Command driven attributes.

Commands need to request the attributes they use, with the API
encouraging them to error on unsupported attributes.

5 files changed, 24 insertions, 24 deletions

diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 11b970d2ef..cab7281719 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -322,14 +322,14 @@ 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 }
+  { add_rewrite_hint ~poly:(only_polymorphism atts) bl o None l }
 | [ "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 }
+  { add_rewrite_hint ~poly:(only_polymorphism atts) bl o (Some t) l }
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
-  { add_rewrite_hint ~poly:atts.polymorphic ["core"] o None 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:atts.polymorphic ["core"] o (Some t) l }
+  { add_rewrite_hint ~poly:(only_polymorphism atts) ["core"] o (Some t) l }
 END
 
 (**********************************************************************)
@@ -414,36 +414,36 @@ VERNAC COMMAND EXTEND DeriveInversionClear
 | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
   => { seff na }
   -> {
-      add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_clear_tac }
+      add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c s false inv_clear_tac }
 
 | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => { seff na }
   -> {
-      add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_clear_tac }
+      add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c Sorts.InProp false inv_clear_tac }
 END
 
 VERNAC COMMAND EXTEND DeriveInversion
 | [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
   => { seff na }
   -> {
-      add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_tac }
+      add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c s false inv_tac }
 
 | [ "Derive" "Inversion" ident(na) "with" constr(c) ] => { seff na }
   -> {
-      add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_tac }
+      add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c Sorts.InProp false inv_tac }
 END
 
 VERNAC COMMAND EXTEND DeriveDependentInversion
 | [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
   => { seff na }
   -> {
-      add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_tac }
+      add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c s true dinv_tac }
 END
 
 VERNAC COMMAND EXTEND DeriveDependentInversionClear
 | [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
   => { seff na }
   -> {
-      add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_clear_tac }
+      add_inversion_lemma_exn ~poly:(only_polymorphism atts) na c s true dinv_clear_tac }
 END
 
 (**********************************************************************)
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 65fa34d712..e8b5e900dd 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -242,7 +242,7 @@ VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
 | [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> {
         let open Attributes in
         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 (only_locality atts))
           (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 f1f3ae74e5..f8842b201c 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -500,10 +500,10 @@ END
 VERNAC COMMAND EXTEND VernacTacticNotation
 | [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] =>
   { VtSideff [], VtNow } ->
-  { let open Attributes 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
+    let deprecation, locality = Attributes.(parse Notations.(deprecation ++ locality) atts) in
+    Tacentries.add_tactic_notation (Locality.make_module_locality locality) n ?deprecation r e;
   }
 END
 
@@ -549,9 +549,9 @@ VERNAC COMMAND EXTEND VernacDeclareTacticDefinition
     VtSideff (List.map (function
       | TacticDefinition ({CAst.v=r},_) -> r
       | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater
-  } -> { let open Attributes in
-           let deprecation = atts.deprecated in
-           Tacentries.register_ltac (Locality.make_module_locality atts.locality) ?deprecation l;
+  } -> {
+         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 32dccf2e83..030b1b5410 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -133,7 +133,7 @@ END
 VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF
 | [ "Obligation" "Tactic" ":=" tactic(t) ] -> {
         set_default_tactic
-          (Locality.make_section_locality atts.Attributes.locality)
+          (Locality.make_section_locality (Attributes.only_locality atts))
           (Tacintern.glob_tactic t);
   }
 END
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 3f12e0e9f9..7880587366 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -273,28 +273,28 @@ END
 VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
   | [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
      {
-         add_setoid (not (Locality.make_section_locality atts.locality)) [] a aeq t n;
+         add_setoid (not (Locality.make_section_locality (only_locality atts))) [] a aeq t n;
      }
   | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
      {
-         add_setoid (not (Locality.make_section_locality atts.locality)) binders a aeq t n;
+         add_setoid (not (Locality.make_section_locality (only_locality atts))) binders a aeq t n;
      }
   | [ "Add" "Morphism" constr(m) ":" ident(n) ]
     (* This command may or may not open a goal *)
     => { Vernacexpr.VtUnknown, Vernacexpr.VtNow }
     -> {
-           add_morphism_infer (not (Locality.make_section_locality atts.locality)) m n;
+           add_morphism_infer (not (Locality.make_section_locality (only_locality atts))) m n;
        }
   | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
     => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) }
     -> {
-           add_morphism (not (Locality.make_section_locality atts.locality)) [] m s n;
+           add_morphism (not (Locality.make_section_locality (only_locality atts))) [] m s n;
        }
   | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
         "with" "signature" lconstr(s) "as" ident(n) ]
     => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) }
     -> {
-           add_morphism (not (Locality.make_section_locality atts.locality)) binders m s n;
+           add_morphism (not (Locality.make_section_locality (only_locality atts))) binders m s n;
        }
 END