From 9e75cacd86d491f81da7171c72569ac0cb6aeae0 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Mon, 26 Feb 2018 08:54:58 +0000
Subject: [vernac] attribute_of_flags

Elaborate a [atts] record out of a list of flags.
---
 stm/vernac_classifier.ml |  7 ++-----
 vernac/vernacentries.ml  | 42 +++++++++++++++++++++---------------------
 vernac/vernacentries.mli |  4 ++++
 3 files changed, 27 insertions(+), 26 deletions(-)

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index e01dcbcb6..0606d27ed 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -199,11 +199,8 @@ let classify_vernac e =
   in
   let rec static_control_classifier ~poly = function
     | VernacExpr (f, e) ->
-      let poly = List.fold_left (fun poly f ->
-          match f with
-          | VernacPolymorphic b -> b
-          | (VernacProgram | VernacLocal _) -> poly
-        ) poly f in
+      let _, atts = Vernacentries.attributes_of_flags f Vernacinterp.{ loc = None ; locality = None ; polymorphic = poly ; program = false } in
+      let poly = atts.Vernacinterp.polymorphic in
       static_classifier ~poly e
     | VernacTimeout (_,e) -> static_control_classifier ~poly e
     | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 5fda1a0da..135141cd4 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2319,32 +2319,32 @@ let with_fail st b f =
       | _ -> assert false
   end
 
+let attributes_of_flags f atts =
+  List.fold_left
+    (fun (polymorphism, atts) f ->
+       match f with
+       | VernacProgram when not atts.program ->
+         (polymorphism, { atts with program = true })
+       | VernacProgram ->
+         user_err Pp.(str "Program mode specified twice")
+       | VernacPolymorphic b when polymorphism = None ->
+         (Some b, atts)
+       | VernacPolymorphic _ ->
+         user_err Pp.(str "Polymorphism specified twice")
+       | VernacLocal b when Option.is_empty atts.locality ->
+         (polymorphism, { atts with locality = Some b })
+       | VernacLocal _ ->
+         user_err Pp.(str "Locality specified twice")
+    )
+    (None, atts)
+    f
+
 let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
   let orig_univ_poly = Flags.is_universe_polymorphism () in
   let orig_program_mode = Flags.is_program_mode () in
-  let flags f atts =
-    List.fold_left
-      (fun (polymorphism, atts) f ->
-         match f with
-         | VernacProgram when not atts.program ->
-           (polymorphism, { atts with program = true })
-         | VernacProgram ->
-           user_err Pp.(str "Program mode specified twice")
-         | VernacPolymorphic b when polymorphism = None ->
-           (Some b, atts)
-         | VernacPolymorphic _ ->
-           user_err Pp.(str "Polymorphism specified twice")
-         | VernacLocal b when Option.is_empty atts.locality ->
-           (polymorphism, { atts with locality = Some b })
-         | VernacLocal _ ->
-           user_err Pp.(str "Locality specified twice")
-      )
-      (None, atts)
-      f
-  in
   let rec control = function
   | VernacExpr (f, v) ->
-    let (polymorphism, atts) = flags f { loc; locality = None; polymorphic = false; program = orig_program_mode; } in
+    let (polymorphism, atts) = attributes_of_flags f { loc; locality = None; polymorphic = false; program = orig_program_mode; } in
     aux ~polymorphism ~atts v
   | VernacFail v -> with_fail st true (fun () -> control v)
   | VernacTimeout (n,v) ->
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 02a3b2bd6..79f9b602a 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -38,3 +38,7 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr
   Evd.evar_map * Redexpr.red_expr) Hook.t
 
 val universe_polymorphism_option_name : string list
+
+(** Elaborate a [atts] record out of a list of flags.
+    Also returns whether polymorphism is explicitly (un)set. *)
+val attributes_of_flags : Vernacexpr.vernac_flag list -> Vernacinterp.atts -> bool option * Vernacinterp.atts
-- 
cgit v1.2.3


From fb9755ab4445fd86cdfc5b249b487629591d87a0 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Thu, 31 May 2018 09:14:47 +0000
Subject: [vernac] mk_atts: an atts record with default values

---
 stm/vernac_classifier.ml | 2 +-
 vernac/vernacentries.ml  | 2 +-
 vernac/vernacinterp.ml   | 3 +++
 vernac/vernacinterp.mli  | 3 +++
 4 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 0606d27ed..6be80d29a 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -199,7 +199,7 @@ let classify_vernac e =
   in
   let rec static_control_classifier ~poly = function
     | VernacExpr (f, e) ->
-      let _, atts = Vernacentries.attributes_of_flags f Vernacinterp.{ loc = None ; locality = None ; polymorphic = poly ; program = false } in
+      let _, atts = Vernacentries.attributes_of_flags f Vernacinterp.(mk_atts ~polymorphic:poly ()) in
       let poly = atts.Vernacinterp.polymorphic in
       static_classifier ~poly e
     | VernacTimeout (_,e) -> static_control_classifier ~poly e
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 135141cd4..1740c5a80 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2344,7 +2344,7 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
   let orig_program_mode = Flags.is_program_mode () in
   let rec control = function
   | VernacExpr (f, v) ->
-    let (polymorphism, atts) = attributes_of_flags f { loc; locality = None; polymorphic = false; program = orig_program_mode; } in
+    let (polymorphism, atts) = attributes_of_flags f (mk_atts ~program:orig_program_mode ()) in
     aux ~polymorphism ~atts v
   | VernacFail v -> with_fail st true (fun () -> control v)
   | VernacTimeout (n,v) ->
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index d4f2a753f..36b8a7e62 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -21,6 +21,9 @@ type atts = {
   program : bool;
 }
 
+let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(program=false) () : atts =
+  { loc ; locality ; polymorphic ; program }
+
 type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
 
 type plugin_args = Genarg.raw_generic_argument list
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index 935cacf77..a24bcd40d 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -19,6 +19,9 @@ type atts = {
   program : bool;
 }
 
+val mk_atts : ?loc: Loc.t option -> ?locality: bool option ->
+  ?polymorphic: bool -> ?program: bool -> unit -> atts
+
 type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
 
 type plugin_args = Genarg.raw_generic_argument list
-- 
cgit v1.2.3


From 8520cc7a02bedf4f4820ef198550f7cfa2a6454c Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Thu, 31 May 2018 08:57:47 +0000
Subject: [vernac] Concrete syntax for attributes

---
 vernac/g_vernac.mlg | 19 ++++++++++++++++++-
 vernac/ppvernac.ml  | 25 +++++++++++++------------
 2 files changed, 31 insertions(+), 13 deletions(-)

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3a01ce6df..bffdaa0b1 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -79,9 +79,26 @@ GRAMMAR EXTEND Gram
       | IDENT "Redirect"; s = ne_string; c = located_vernac -> { VernacRedirect (s, c) }
       | IDENT "Timeout"; n = natural; v = vernac_control -> { VernacTimeout(n,v) }
       | IDENT "Fail"; v = vernac_control -> { VernacFail v }
-      | v = vernac -> { let (f, v) = v in VernacExpr(f, v) } ]
+      | v = decorated_vernac -> { let (f, v) = v in VernacExpr(f, v) } ]
     ]
   ;
+  decorated_vernac:
+  [[ a = attributes ; fv = vernac -> let (f, v) = fv in (List.append a f, v)
+  | fv = vernac -> fv
+  ]]
+  ;
+  attributes: [[ "#[" ; a = LIST1 attribute SEP "," ; "]" -> a ]]
+  ;
+  attribute:
+  [[
+    IDENT "polymorphic" -> VernacPolymorphic true
+  | IDENT "monomorphic" -> VernacPolymorphic false
+  | IDENT "program" -> VernacProgram
+  | IDENT "local" -> VernacLocal true
+  | IDENT "global" -> VernacLocal false
+  | IDENT "coercion" -> VernacCoercion
+  ]]
+  ;
   vernac:
     [ [ IDENT "Local"; v = vernac_poly -> { let (f, v) = v in (VernacLocal true :: f, v) }
       | IDENT "Global"; v = vernac_poly -> { let (f, v) = v in (VernacLocal false :: f, v) }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 5fbe1f4e4..b49fb011b 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -153,8 +153,6 @@ open Pputils
       | SearchAbout sl ->
          keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b
 
-  let pr_locality local = if local then keyword "Local" else keyword "Global"
-
   let pr_option_ref_value = function
     | QualidRefValue id -> pr_qualid id
     | StringRefValue s -> qs s
@@ -1195,21 +1193,24 @@ open Pputils
       | VernacEndSubproof ->
         return (str "}")
 
-let pr_vernac_flag =
+let pr_vernac_flag f =
+  keyword (match f with
+  | VernacPolymorphic true -> "polymorphic"
+  | VernacPolymorphic false -> "monomorphic"
+  | VernacProgram -> "program"
+  | VernacLocal true -> "local"
+  | VernacLocal false -> "global"
+  )
+
+let pr_vernac_flag_list =
   function
-  | VernacPolymorphic true -> keyword "Polymorphic"
-  | VernacPolymorphic false -> keyword "Monomorphic"
-  | VernacProgram -> keyword "Program"
-  | VernacLocal local -> pr_locality local
+  | [] -> mt ()
+  | flags ->  str "#[" ++ prlist_with_sep (fun () -> str ", ") pr_vernac_flag flags ++ str "]" ++ cut ()
 
   let rec pr_vernac_control v =
     let return = tag_vernac v in
     match v with
-    | VernacExpr (f, v') ->
-      List.fold_right
-        (fun f a -> pr_vernac_flag f ++ spc() ++ a)
-        f
-        (pr_vernac_expr v' ++ sep_end v')
+    | VernacExpr (f, v') -> pr_vernac_flag_list f ++ pr_vernac_expr v' ++ sep_end v'
     | VernacTime (_,{v}) ->
       return (keyword "Time" ++ spc() ++ pr_vernac_control v)
     | VernacRedirect (s, {v}) ->
-- 
cgit v1.2.3


From 767898e6e59e86e3123846374448402360b783e6 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Thu, 31 May 2018 12:39:38 +0000
Subject: Allow “Let”-defined coercions
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 vernac/class.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/vernac/class.ml b/vernac/class.ml
index 133726702..e425e6474 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -303,12 +303,12 @@ let try_add_new_coercion_with_source ref ~local poly ~source =
   try_add_new_coercion_core ref ~local poly (Some source) None false
 
 let add_coercion_hook poly local ref =
-  let stre = match local with
+  let local = match local with
+  | Discharge
   | Local -> true
   | Global -> false
-  | Discharge -> assert false
   in
-  let () = try_add_new_coercion ref ~local:stre poly in
+  let () = try_add_new_coercion ref ~local poly in
   let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
   Flags.if_verbose Feedback.msg_info msg
 
-- 
cgit v1.2.3


From 5494c46f6219bea902fcc5ed983e16d1105fec51 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Mon, 25 Jun 2018 08:00:47 +0000
Subject: [vernac] Add a “deprecated” attribute
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 vernac/ppvernac.ml      | 24 +++++++++++++++++-------
 vernac/vernacentries.ml |  4 ++++
 vernac/vernacexpr.ml    |  1 +
 vernac/vernacinterp.ml  |  5 +++--
 vernac/vernacinterp.mli |  3 ++-
 5 files changed, 27 insertions(+), 10 deletions(-)

diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index b49fb011b..f9237c775 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1193,14 +1193,24 @@ open Pputils
       | VernacEndSubproof ->
         return (str "}")
 
+let rec pr_vernac_flag_data (k, v) =
+  let k = keyword k in
+  match v with
+  | `Empty -> k
+  | `Leaf v -> k ++ str " = " ++ qs v
+  | `Node m -> k ++ str "( " ++ prlist_with_sep (fun () -> str ", ") pr_vernac_flag_data m ++ str " )"
+
 let pr_vernac_flag f =
-  keyword (match f with
-  | VernacPolymorphic true -> "polymorphic"
-  | VernacPolymorphic false -> "monomorphic"
-  | VernacProgram -> "program"
-  | VernacLocal true -> "local"
-  | VernacLocal false -> "global"
-  )
+  match f with
+  | VernacPolymorphic true -> keyword "polymorphic"
+  | VernacPolymorphic false -> keyword "monomorphic"
+  | VernacProgram -> keyword "program"
+  | VernacLocal true -> keyword "local"
+  | VernacLocal false -> keyword "global"
+  | VernacDeprecated (since, note) ->
+    pr_vernac_flag_data ("deprecated", `Node [
+        "since", `Leaf since; "note", `Leaf note
+      ])
 
 let pr_vernac_flag_list =
   function
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 1740c5a80..af0f19834 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2335,6 +2335,10 @@ let attributes_of_flags f atts =
          (polymorphism, { atts with locality = Some b })
        | VernacLocal _ ->
          user_err Pp.(str "Locality specified twice")
+       | VernacDeprecated (since, note) when Option.is_empty atts.deprecated ->
+         (polymorphism, { atts with deprecated = Some (since, note) })
+       | VernacDeprecated _ ->
+         user_err Pp.(str "Deprecation specified twice")
     )
     (None, atts)
     f
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index f5f37339c..57ccb6006 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -463,6 +463,7 @@ type nonrec vernac_flag =
   | VernacProgram
   | VernacPolymorphic of bool
   | VernacLocal of bool
+  | VernacDeprecated of string * string (* Since, Note *)
 
 type vernac_control =
   | VernacExpr of vernac_flag list * vernac_expr
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 36b8a7e62..30c1ddbfd 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -19,10 +19,11 @@ type atts = {
   locality : bool option;
   polymorphic : bool;
   program : bool;
+  deprecated : (string * string) option;
 }
 
-let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(program=false) () : atts =
-  { loc ; locality ; polymorphic ; program }
+let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(program=false) ?(deprecated=None) () : atts =
+  { loc ; locality ; polymorphic ; program ; deprecated }
 
 type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
 
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index a24bcd40d..362c05d4c 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -17,10 +17,11 @@ type atts = {
   locality : bool option;
   polymorphic : bool;
   program : bool;
+  deprecated : (string * string) option; (* Since, Note *)
 }
 
 val mk_atts : ?loc: Loc.t option -> ?locality: bool option ->
-  ?polymorphic: bool -> ?program: bool -> unit -> atts
+  ?polymorphic: bool -> ?program: bool -> ?deprecated: (string * string) option -> unit -> atts
 
 type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
 
-- 
cgit v1.2.3


From 3c83ca8b3ea9ec3ea6656dc7f726c46a21729541 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Mon, 25 Jun 2018 08:52:29 +0000
Subject: [vernac] Generic parsing rules for attributes

---
 vernac/g_vernac.mlg | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index bffdaa0b1..49fcda849 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -97,6 +97,20 @@ GRAMMAR EXTEND Gram
   | IDENT "local" -> VernacLocal true
   | IDENT "global" -> VernacLocal false
   | IDENT "coercion" -> VernacCoercion
+  | IDENT "deprecated" ; v = attribute_value ->
+    match v with
+    | `List [ k1, `Leaf since ; k2, `Leaf note ] when Names.Id.equal k1 (Names.Id.of_string "since") && Names.Id.equal k2 (Names.Id.of_string "note") -> VernacDeprecated (since, note)
+    |  _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute")
+  ]]
+  ;
+  attribute_value:
+  [[ "=" ; v = string -> `Leaf v
+   | "(" ; m = LIST0 attribute_pair SEP "," ; ")" -> `List m
+   | -> `Empty
+  ]]
+  ;
+  attribute_pair:
+  [[ k = ident ; v = attribute_value -> (k, v)
   ]]
   ;
   vernac:
-- 
cgit v1.2.3


From 4371ff2357c11d913b163dde193255f538f3565f Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Mon, 25 Jun 2018 09:35:25 +0000
Subject: [vernac] Generic syntax for flags/attributes

---
 vernac/g_vernac.mlg      | 42 +++++++++++++++++-------------------------
 vernac/ppvernac.ml       | 32 +++++++++++---------------------
 vernac/vernacentries.ml  | 46 +++++++++++++++++++++++++++++++++-------------
 vernac/vernacentries.mli |  2 +-
 vernac/vernacexpr.ml     | 12 ++++++------
 5 files changed, 68 insertions(+), 66 deletions(-)

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 49fcda849..92c685741 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -87,50 +87,42 @@ GRAMMAR EXTEND Gram
   | fv = vernac -> fv
   ]]
   ;
-  attributes: [[ "#[" ; a = LIST1 attribute SEP "," ; "]" -> a ]]
-  ;
-  attribute:
-  [[
-    IDENT "polymorphic" -> VernacPolymorphic true
-  | IDENT "monomorphic" -> VernacPolymorphic false
-  | IDENT "program" -> VernacProgram
-  | IDENT "local" -> VernacLocal true
-  | IDENT "global" -> VernacLocal false
-  | IDENT "coercion" -> VernacCoercion
-  | IDENT "deprecated" ; v = attribute_value ->
-    match v with
-    | `List [ k1, `Leaf since ; k2, `Leaf note ] when Names.Id.equal k1 (Names.Id.of_string "since") && Names.Id.equal k2 (Names.Id.of_string "note") -> VernacDeprecated (since, note)
-    |  _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute")
+  attributes:
+  [[ "#[" ; a = attribute_list ; "]" -> a
   ]]
   ;
-  attribute_value:
-  [[ "=" ; v = string -> `Leaf v
-   | "(" ; m = LIST0 attribute_pair SEP "," ; ")" -> `List m
-   | -> `Empty
+  attribute_list:
+  [[ a = LIST0 attribute SEP "," -> a
   ]]
   ;
-  attribute_pair:
+  attribute:
   [[ k = ident ; v = attribute_value -> (k, v)
   ]]
   ;
+  attribute_value:
+  [[ "=" ; v = string -> VernacFlagLeaf v
+   | "(" ; a = attribute_list ; ")" -> VernacFlagList a
+   | -> VernacFlagEmpty
+  ]]
+  ;
   vernac:
-    [ [ IDENT "Local"; v = vernac_poly -> { let (f, v) = v in (VernacLocal true :: f, v) }
-      | IDENT "Global"; v = vernac_poly -> { let (f, v) = v in (VernacLocal false :: f, v) }
+    [ [ IDENT "Local"; v = vernac_poly -> { let (f, v) = v in ((Names.Id.of_string "local", VernacFlagEmpty) :: f, v) }
+      | IDENT "Global"; v = vernac_poly -> { let (f, v) = v in ((Names.Id.of_string "global", VernacFlagEmpty) :: f, v) }
 
       | v = vernac_poly -> { v } ]
     ]
   ;
   vernac_poly:
-    [ [ IDENT "Polymorphic"; v = vernac_aux -> { let (f, v) = v in (VernacPolymorphic true :: f, v) }
-      | IDENT "Monomorphic"; v = vernac_aux -> { let (f, v) = v in (VernacPolymorphic false :: f, v) }
+    [ [ IDENT "Polymorphic"; v = vernac_aux -> { let (f, v) = v in ((Names.Id.of_string "polymorphic", VernacFlagEmpty) :: f, v) }
+      | IDENT "Monomorphic"; v = vernac_aux -> { let (f, v) = v in ((Names.Id.of_string "monomorphic", VernacFlagEmpty) :: f, v) }
       | v = vernac_aux -> { v } ]
     ]
   ;
   vernac_aux:
     (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
     (* "." is still in the stream and discard_to_dot works correctly         *)
-    [ [ IDENT "Program"; g = gallina; "." -> { ([VernacProgram], g) }
-      | IDENT "Program"; g = gallina_ext; "." -> { ([VernacProgram], g) }
+    [ [ IDENT "Program"; g = gallina; "." -> { ([Names.Id.of_string "program", VernacFlagEmpty], g) }
+      | IDENT "Program"; g = gallina_ext; "." -> { ([Names.Id.of_string "program", VernacFlagEmpty], g) }
       | g = gallina; "." -> { ([], g) }
       | g = gallina_ext; "." -> { ([], g) }
       | c = command; "." -> { ([], c) }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index f9237c775..024c145aa 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1193,34 +1193,24 @@ open Pputils
       | VernacEndSubproof ->
         return (str "}")
 
-let rec pr_vernac_flag_data (k, v) =
-  let k = keyword k in
+let rec pr_vernac_flag (k, v) =
+  let k = keyword (Names.Id.to_string k) in
   match v with
-  | `Empty -> k
-  | `Leaf v -> k ++ str " = " ++ qs v
-  | `Node m -> k ++ str "( " ++ prlist_with_sep (fun () -> str ", ") pr_vernac_flag_data m ++ str " )"
-
-let pr_vernac_flag f =
-  match f with
-  | VernacPolymorphic true -> keyword "polymorphic"
-  | VernacPolymorphic false -> keyword "monomorphic"
-  | VernacProgram -> keyword "program"
-  | VernacLocal true -> keyword "local"
-  | VernacLocal false -> keyword "global"
-  | VernacDeprecated (since, note) ->
-    pr_vernac_flag_data ("deprecated", `Node [
-        "since", `Leaf since; "note", `Leaf note
-      ])
-
-let pr_vernac_flag_list =
+  | VernacFlagEmpty -> k
+  | VernacFlagLeaf v -> k ++ str " = " ++ qs v
+  | VernacFlagList m -> k ++ str "( " ++ pr_vernac_flags m ++ str " )"
+and pr_vernac_flags m =
+  prlist_with_sep (fun () -> str ", ") pr_vernac_flag m
+
+let pr_vernac_attributes =
   function
   | [] -> mt ()
-  | flags ->  str "#[" ++ prlist_with_sep (fun () -> str ", ") pr_vernac_flag flags ++ str "]" ++ cut ()
+  | flags ->  str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut ()
 
   let rec pr_vernac_control v =
     let return = tag_vernac v in
     match v with
-    | VernacExpr (f, v') -> pr_vernac_flag_list f ++ pr_vernac_expr v' ++ sep_end v'
+    | VernacExpr (f, v') -> pr_vernac_attributes f ++ pr_vernac_expr v' ++ sep_end v'
     | VernacTime (_,{v}) ->
       return (keyword "Time" ++ spc() ++ pr_vernac_control v)
     | VernacRedirect (s, {v}) ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index af0f19834..e61687290 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2320,25 +2320,45 @@ let with_fail st b f =
   end
 
 let attributes_of_flags f atts =
+  let assert_empty k v =
+    if v <> VernacFlagEmpty
+    then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments")
+  in
   List.fold_left
-    (fun (polymorphism, atts) f ->
-       match f with
-       | VernacProgram when not atts.program ->
+    (fun (polymorphism, atts) (k, v) ->
+       let k = Names.Id.to_string k in
+       match k with
+       | "program" when not atts.program ->
+         assert_empty k v;
          (polymorphism, { atts with program = true })
-       | VernacProgram ->
+       | "program" ->
          user_err Pp.(str "Program mode specified twice")
-       | VernacPolymorphic b when polymorphism = None ->
-         (Some b, atts)
-       | VernacPolymorphic _ ->
+       | "polymorphic" when polymorphism = None ->
+         assert_empty k v;
+         (Some true, atts)
+       | "monomorphic" when polymorphism = None ->
+         assert_empty k v;
+         (Some false, atts)
+       | ("polymorphic" | "monomorphic") ->
          user_err Pp.(str "Polymorphism specified twice")
-       | VernacLocal b when Option.is_empty atts.locality ->
-         (polymorphism, { atts with locality = Some b })
-       | VernacLocal _ ->
+       | "local" when Option.is_empty atts.locality ->
+         assert_empty k v;
+         (polymorphism, { atts with locality = Some true })
+       | "global" when Option.is_empty atts.locality ->
+         assert_empty k v;
+         (polymorphism, { atts with locality = Some false })
+       | ("local" | "global") ->
          user_err Pp.(str "Locality specified twice")
-       | VernacDeprecated (since, note) when Option.is_empty atts.deprecated ->
-         (polymorphism, { atts with deprecated = Some (since, note) })
-       | VernacDeprecated _ ->
+       | "deprecated" when Option.is_empty atts.deprecated ->
+           begin match v with
+             | VernacFlagList [ k1, VernacFlagLeaf since ; k2, VernacFlagLeaf note ]
+               when Names.Id.(equal k1 (of_string "since") && equal k2 (of_string "note")) ->
+               (polymorphism, { atts with deprecated = Some (since, note) })
+             |  _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute")
+           end
+       | "deprecated" ->
          user_err Pp.(str "Deprecation specified twice")
+       | _ -> user_err Pp.(str "Unknown attribute " ++ str k)
     )
     (None, atts)
     f
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 79f9b602a..79f9c05ad 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -41,4 +41,4 @@ val universe_polymorphism_option_name : string list
 
 (** Elaborate a [atts] record out of a list of flags.
     Also returns whether polymorphism is explicitly (un)set. *)
-val attributes_of_flags : Vernacexpr.vernac_flag list -> Vernacinterp.atts -> bool option * Vernacinterp.atts
+val attributes_of_flags : Vernacexpr.vernac_flags -> Vernacinterp.atts -> bool option * Vernacinterp.atts
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 57ccb6006..2287630c7 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -459,14 +459,14 @@ type nonrec vernac_expr =
   (* For extension *)
   | VernacExtend of extend_name * Genarg.raw_generic_argument list
 
-type nonrec vernac_flag =
-  | VernacProgram
-  | VernacPolymorphic of bool
-  | VernacLocal of bool
-  | VernacDeprecated of string * string (* Since, Note *)
+type vernac_flags = (Names.Id.t * vernac_flag_value) list
+and vernac_flag_value =
+  | VernacFlagEmpty
+  | VernacFlagLeaf of string
+  | VernacFlagList of vernac_flags
 
 type vernac_control =
-  | VernacExpr of vernac_flag list * vernac_expr
+  | VernacExpr of vernac_flags * vernac_expr
   (* boolean is true when the `-time` batch-mode command line flag was set.
      the flag is used to print differently in `-time` vs `Time foo` *)
   | VernacTime of bool * vernac_control CAst.t
-- 
cgit v1.2.3


From 0a0e956929e28fd6f1c43f39d7b92aeeaf0f01e2 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Mon, 25 Jun 2018 16:02:02 +0000
Subject: [vernac] indentation

---
 vernac/g_vernac.mlg | 26 +++++++++++++-------------
 1 file changed, 13 insertions(+), 13 deletions(-)

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 92c685741..23b6898c3 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -83,27 +83,27 @@ GRAMMAR EXTEND Gram
     ]
   ;
   decorated_vernac:
-  [[ a = attributes ; fv = vernac -> let (f, v) = fv in (List.append a f, v)
-  | fv = vernac -> fv
-  ]]
+    [ [ a = attributes ; fv = vernac -> let (f, v) = fv in (List.append a f, v)
+      | fv = vernac -> fv ]
+    ]
   ;
   attributes:
-  [[ "#[" ; a = attribute_list ; "]" -> a
-  ]]
+    [ [ "#[" ; a = attribute_list ; "]" -> a ]
+    ]
   ;
   attribute_list:
-  [[ a = LIST0 attribute SEP "," -> a
-  ]]
+    [ [ a = LIST0 attribute SEP "," -> a ]
+    ]
   ;
   attribute:
-  [[ k = ident ; v = attribute_value -> (k, v)
-  ]]
+    [ [ k = ident ; v = attribute_value -> (k, v) ]
+    ]
   ;
   attribute_value:
-  [[ "=" ; v = string -> VernacFlagLeaf v
-   | "(" ; a = attribute_list ; ")" -> VernacFlagList a
-   | -> VernacFlagEmpty
-  ]]
+    [ [ "=" ; v = string -> VernacFlagLeaf v
+      | "(" ; a = attribute_list ; ")" -> VernacFlagList a
+      | -> VernacFlagEmpty ]
+    ]
   ;
   vernac:
     [ [ IDENT "Local"; v = vernac_poly -> { let (f, v) = v in ((Names.Id.of_string "local", VernacFlagEmpty) :: f, v) }
-- 
cgit v1.2.3


From d3127693d4a2125088aa512f593d782843482f2a Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Mon, 25 Jun 2018 16:09:11 +0000
Subject: [vernac] use plain strings as attribute names

The concrete syntax is still restricted to identifiers.
---
 vernac/g_vernac.mlg     | 14 +++++++-------
 vernac/ppvernac.ml      |  2 +-
 vernac/vernacentries.ml |  5 ++---
 vernac/vernacexpr.ml    |  2 +-
 4 files changed, 11 insertions(+), 12 deletions(-)

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 23b6898c3..3afe3391b 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -96,7 +96,7 @@ GRAMMAR EXTEND Gram
     ]
   ;
   attribute:
-    [ [ k = ident ; v = attribute_value -> (k, v) ]
+    [ [ k = ident ; v = attribute_value -> (Names.Id.to_string k, v) ]
     ]
   ;
   attribute_value:
@@ -106,23 +106,23 @@ GRAMMAR EXTEND Gram
     ]
   ;
   vernac:
-    [ [ IDENT "Local"; v = vernac_poly -> { let (f, v) = v in ((Names.Id.of_string "local", VernacFlagEmpty) :: f, v) }
-      | IDENT "Global"; v = vernac_poly -> { let (f, v) = v in ((Names.Id.of_string "global", VernacFlagEmpty) :: f, v) }
+    [ [ IDENT "Local"; v = vernac_poly -> { let (f, v) = v in (("local", VernacFlagEmpty) :: f, v) }
+      | IDENT "Global"; v = vernac_poly -> { let (f, v) = v in (("global", VernacFlagEmpty) :: f, v) }
 
       | v = vernac_poly -> { v } ]
     ]
   ;
   vernac_poly:
-    [ [ IDENT "Polymorphic"; v = vernac_aux -> { let (f, v) = v in ((Names.Id.of_string "polymorphic", VernacFlagEmpty) :: f, v) }
-      | IDENT "Monomorphic"; v = vernac_aux -> { let (f, v) = v in ((Names.Id.of_string "monomorphic", VernacFlagEmpty) :: f, v) }
+    [ [ IDENT "Polymorphic"; v = vernac_aux -> { let (f, v) = v in (("polymorphic", VernacFlagEmpty) :: f, v) }
+      | IDENT "Monomorphic"; v = vernac_aux -> { let (f, v) = v in (("monomorphic", VernacFlagEmpty) :: f, v) }
       | v = vernac_aux -> { v } ]
     ]
   ;
   vernac_aux:
     (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
     (* "." is still in the stream and discard_to_dot works correctly         *)
-    [ [ IDENT "Program"; g = gallina; "." -> { ([Names.Id.of_string "program", VernacFlagEmpty], g) }
-      | IDENT "Program"; g = gallina_ext; "." -> { ([Names.Id.of_string "program", VernacFlagEmpty], g) }
+    [ [ IDENT "Program"; g = gallina; "." -> { (["program", VernacFlagEmpty], g) }
+      | IDENT "Program"; g = gallina_ext; "." -> { (["program", VernacFlagEmpty], g) }
       | g = gallina; "." -> { ([], g) }
       | g = gallina_ext; "." -> { ([], g) }
       | c = command; "." -> { ([], c) }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 024c145aa..e5547d9b7 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1194,7 +1194,7 @@ open Pputils
         return (str "}")
 
 let rec pr_vernac_flag (k, v) =
-  let k = keyword (Names.Id.to_string k) in
+  let k = keyword k in
   match v with
   | VernacFlagEmpty -> k
   | VernacFlagLeaf v -> k ++ str " = " ++ qs v
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e61687290..080d42607 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2326,7 +2326,6 @@ let attributes_of_flags f atts =
   in
   List.fold_left
     (fun (polymorphism, atts) (k, v) ->
-       let k = Names.Id.to_string k in
        match k with
        | "program" when not atts.program ->
          assert_empty k v;
@@ -2351,8 +2350,8 @@ let attributes_of_flags f atts =
          user_err Pp.(str "Locality specified twice")
        | "deprecated" when Option.is_empty atts.deprecated ->
            begin match v with
-             | VernacFlagList [ k1, VernacFlagLeaf since ; k2, VernacFlagLeaf note ]
-               when Names.Id.(equal k1 (of_string "since") && equal k2 (of_string "note")) ->
+             | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ]
+             | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] ->
                (polymorphism, { atts with deprecated = Some (since, note) })
              |  _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute")
            end
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 2287630c7..e97cac818 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -459,7 +459,7 @@ type nonrec vernac_expr =
   (* For extension *)
   | VernacExtend of extend_name * Genarg.raw_generic_argument list
 
-type vernac_flags = (Names.Id.t * vernac_flag_value) list
+type vernac_flags = (string * vernac_flag_value) list
 and vernac_flag_value =
   | VernacFlagEmpty
   | VernacFlagLeaf of string
-- 
cgit v1.2.3


From f0e546fdb98ff7244d5c393c739f5b7238295918 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Wed, 27 Jun 2018 17:40:48 +0000
Subject: [vernac] use a record for the contents of the “deprecated” attribute
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 vernac/vernacentries.ml |  9 ++++++++-
 vernac/vernacinterp.ml  |  9 ++++++---
 vernac/vernacinterp.mli | 10 ++++++----
 3 files changed, 20 insertions(+), 8 deletions(-)

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 080d42607..27f2a740e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2352,7 +2352,14 @@ let attributes_of_flags f atts =
            begin match v with
              | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ]
              | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] ->
-               (polymorphism, { atts with deprecated = Some (since, note) })
+               let since = Some since and note = Some note in
+               (polymorphism, { atts with deprecated = Some (mk_deprecation ~since ~note ()) })
+             | VernacFlagList [ "since", VernacFlagLeaf since ] ->
+               let since = Some since in
+               (polymorphism, { atts with deprecated = Some (mk_deprecation ~since ()) })
+             | VernacFlagList [ "note", VernacFlagLeaf note ] ->
+               let note = Some note in
+               (polymorphism, { atts with deprecated = Some (mk_deprecation ~note ()) })
              |  _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute")
            end
        | "deprecated" ->
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 30c1ddbfd..1bb1414f3 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -12,14 +12,17 @@ open Util
 open Pp
 open CErrors
 
-type deprecation = bool
+type deprecation = { since : string option ; note : string option }
+
+let mk_deprecation ?(since=None) ?(note=None) () =
+  { since ; note }
 
 type atts = {
   loc : Loc.t option;
   locality : bool option;
   polymorphic : bool;
   program : bool;
-  deprecated : (string * string) option;
+  deprecated : deprecation option;
 }
 
 let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(program=false) ?(deprecated=None) () : atts =
@@ -32,7 +35,7 @@ type plugin_args = Genarg.raw_generic_argument list
 (* Table of vernac entries *)
 let vernac_tab =
   (Hashtbl.create 211 :
-    (Vernacexpr.extend_name, deprecation * plugin_args vernac_command) Hashtbl.t)
+    (Vernacexpr.extend_name, bool * plugin_args vernac_command) Hashtbl.t)
 
 let vinterp_add depr s f =
   try
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index 362c05d4c..46468b309 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -10,25 +10,27 @@
 
 (** Interpretation of extended vernac phrases. *)
 
-type deprecation = bool
+type deprecation = { since : string option ; note : string option }
+
+val mk_deprecation : ?since: string option -> ?note: string option -> unit -> deprecation
 
 type atts = {
   loc : Loc.t option;
   locality : bool option;
   polymorphic : bool;
   program : bool;
-  deprecated : (string * string) option; (* Since, Note *)
+  deprecated : deprecation option;
 }
 
 val mk_atts : ?loc: Loc.t option -> ?locality: bool option ->
-  ?polymorphic: bool -> ?program: bool -> ?deprecated: (string * string) option -> unit -> atts
+  ?polymorphic: bool -> ?program: bool -> ?deprecated: deprecation option -> unit -> atts
 
 type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
 
 type plugin_args = Genarg.raw_generic_argument list
 
 val vinterp_init : unit -> unit
-val vinterp_add : deprecation -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit
+val vinterp_add : bool -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit
 val overwriting_vinterp_add : Vernacexpr.extend_name -> plugin_args vernac_command -> unit
 
 val call : Vernacexpr.extend_name -> plugin_args -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
-- 
cgit v1.2.3


From 1615f76645b0307485ee3143b0d185e91a4935b5 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Mon, 2 Jul 2018 13:47:21 +0000
Subject: Describe attributes in the documentation.

---
 .../language/gallina-specification-language.rst    | 61 +++++++++++++++++++++-
 1 file changed, 60 insertions(+), 1 deletion(-)

diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index e13625286..ac6a20198 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -103,7 +103,7 @@ Special tokens
     ! % & && ( () ) * + ++ , - -> . .( ..
     / /\ : :: :< := :> ; < <- <-> <: <= <> =
     => =_D > >-> >= ? ?= @ [ \/ ] ^ { | |-
-    || } ~
+    || } ~ #[
 
   Lexical ambiguities are resolved according to the “longest match”
   rule: when a sequence of non alphanumerical characters can be
@@ -495,6 +495,7 @@ The Vernacular
 ==============
 
 .. productionlist:: coq
+   decorated-sentence : [`decoration`] `sentence`
    sentence           : `assumption`
                       : | `definition`
                       : | `inductive`
@@ -523,6 +524,11 @@ The Vernacular
    proof              : Proof . … Qed .
                       : | Proof . … Defined .
                       : | Proof . … Admitted .
+   decoration : #[ `attributes` ]
+   attributes : [`attribute`, … , `attribute`]
+   attribute :  `ident`
+   :| `ident` = `string`
+   :| `ident` ( `attributes` )
 
 .. todo:: This use of … in this grammar is inconsistent
           What about removing the proof part of this grammar from this chapter
@@ -534,6 +540,9 @@ commands of Gallina. A sentence of the vernacular language, like in
 many natural languages, begins with a capital letter and ends with a
 dot.
 
+Sentences may be *decorated* with so-called *attributes*,
+which are described in the corresponding section (:ref:`gallina-attributes`).
+
 The different kinds of command are described hereafter. They all suppose
 that the terms occurring in the sentences are well-typed.
 
@@ -1388,3 +1397,53 @@ using the keyword :cmd:`Qed`.
 .. [2]
    Except if the inductive type is empty in which case there is no
    equation that can be used to infer the return type.
+
+.. _gallina-attributes:
+
+Attributes
+-----------
+
+Any vernacular command can be decorated with a list of attributes, enclosed
+between ``#[`` (hash and opening square bracket) and ``]`` (closing square bracket)
+and separated by commas ``,``.
+
+Each attribute has a name (an identifier) and may have a value.
+A value is either a :token:`string` (in which case it is specified with an equal ``=`` sign),
+or a list of attributes, enclosed within brackets.
+
+Currently,
+the following attributes names are recognized:
+
+``monomorphic``, ``polymorphic``
+    Take no value, analogous to the ``Monomorphic`` and ``Polymorphic`` flags
+    (see :ref:`polymorphicuniverses`).
+
+``program``
+    Takes no value, analogous to the ``Program`` flag
+    (see :ref:`programs`).
+
+``global``, ``local``
+    Take no value, analogous to the ``Global`` and ``Local`` flags
+    (see :ref:`controlling-locality-of-commands`).
+
+``deprecated``
+    Takes as value the optional attributes ``since`` and ``note``;
+    both have a string value.
+
+Here are a few examples:
+
+.. coqtop:: all reset
+
+        From Coq Require Program.
+        #[program] Definition one : nat := S _.
+        Next Obligation.
+          exact O.
+        Defined.
+
+        #[deprecated(since="8.9.0", note="use idtac instead")]
+        Ltac foo := idtac.
+
+        Goal True.
+        Proof.
+          now foo.
+        Abort.
-- 
cgit v1.2.3


From 1a4d29ea194833d337ff23320c56e7f324fa82b7 Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Tue, 3 Jul 2018 16:25:52 +0000
Subject: fix syntax of .mlg

---
 vernac/g_vernac.mlg | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3afe3391b..e9d6ed9f6 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -83,26 +83,26 @@ GRAMMAR EXTEND Gram
     ]
   ;
   decorated_vernac:
-    [ [ a = attributes ; fv = vernac -> let (f, v) = fv in (List.append a f, v)
-      | fv = vernac -> fv ]
+    [ [ a = attributes ; fv = vernac -> { let (f, v) = fv in (List.append a f, v) }
+      | fv = vernac -> { fv } ]
     ]
   ;
   attributes:
-    [ [ "#[" ; a = attribute_list ; "]" -> a ]
+    [ [ "#[" ; a = attribute_list ; "]" -> { a } ]
     ]
   ;
   attribute_list:
-    [ [ a = LIST0 attribute SEP "," -> a ]
+    [ [ a = LIST0 attribute SEP "," -> { a } ]
     ]
   ;
   attribute:
-    [ [ k = ident ; v = attribute_value -> (Names.Id.to_string k, v) ]
+    [ [ k = ident ; v = attribute_value -> { Names.Id.to_string k, v } ]
     ]
   ;
   attribute_value:
-    [ [ "=" ; v = string -> VernacFlagLeaf v
-      | "(" ; a = attribute_list ; ")" -> VernacFlagList a
-      | -> VernacFlagEmpty ]
+    [ [ "=" ; v = string -> { VernacFlagLeaf v }
+      | "(" ; a = attribute_list ; ")" -> { VernacFlagList a }
+      | -> { VernacFlagEmpty } ]
     ]
   ;
   vernac:
-- 
cgit v1.2.3


From cda674b91ec137bb4c995063888cc5059884ac8c Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Tue, 3 Jul 2018 16:52:12 +0000
Subject: Document attributes.

---
 CHANGES | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGES b/CHANGES
index 3ec53fad2..0a5ac56b7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -58,6 +58,8 @@ Vernacular Commands
 - New Set Hint Variables/Constants Opaque/Transparent commands for setting
   globally the opacity flag of variables and constants in hint databases,
   overwritting the opacity set of the hint database.
+- Added generic syntax for “attributes”, as in:
+  `#[local] Lemma foo : bar.`
 
 Coq binaries and process model
 
-- 
cgit v1.2.3


From 420b38cba7aedfcfeac5671a7db0c02c4bb14a0c Mon Sep 17 00:00:00 2001
From: Vincent Laporte <Vincent.Laporte@gmail.com>
Date: Tue, 3 Jul 2018 17:06:03 +0000
Subject: [test suite] Test case for attributes

---
 test-suite/success/attribute-syntax.v | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)
 create mode 100644 test-suite/success/attribute-syntax.v

diff --git a/test-suite/success/attribute-syntax.v b/test-suite/success/attribute-syntax.v
new file mode 100644
index 000000000..83fb3d0c8
--- /dev/null
+++ b/test-suite/success/attribute-syntax.v
@@ -0,0 +1,23 @@
+From Coq Require Program.
+
+Section Scope.
+
+#[local] Coercion nat_of_bool (b: bool) : nat :=
+  if b then 0 else 1.
+
+Check (refl_equal : true = 0 :> nat).
+
+End Scope.
+
+Fail Check 0 = true :> nat.
+
+#[polymorphic]
+Definition ι T (x: T) := x.
+
+Check ι _ ι.
+
+#[program]
+Fixpoint f (n: nat) {wf lt n} : nat := _.
+
+#[deprecated(since="8.9.0")]
+Ltac foo := foo.
-- 
cgit v1.2.3