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
~~~

1 files changed, 2 insertions, 3 deletions

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