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

4 files changed, 70 insertions, 8 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 }