Command driven attributes.

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

16 files changed, 245 insertions, 125 deletions

diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 5a4cda54b2..14a3acad57 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -76,7 +76,7 @@ VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
 | [ "Set" "Firstorder" "Solver" tactic(t) ] -> {
     let open Attributes in
       set_default_solver
-        (Locality.make_section_locality atts.locality)
+        (Locality.make_section_locality (only_locality atts))
         (Tacintern.glob_tactic t)
   }
 END
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
 
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 2f44624d36..2774b843aa 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -173,7 +173,7 @@ VERNAC COMMAND EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF
   | [ "Prenex" "Implicits" ne_global_list(fl) ]
   -> {
          let open Attributes in
-         let locality = Locality.make_section_locality atts.locality in
+         let locality = Locality.make_section_locality (only_locality atts) 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 54764d541f..e70edd56cb 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 Attributes
 open Ltac_plugin
 open Stdarg
 open Pcoq.Prim
@@ -38,5 +37,5 @@ END
 VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
   | [ "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 (Attributes.only_locality atts)) ty f g (Id.to_string sc) o }
 END
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 037c63ef03..4958f17212 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -194,9 +194,8 @@ let classify_vernac e =
   in
   let rec static_control_classifier ~poly = function
     | VernacExpr (f, e) ->
-      let _, atts = Attributes.attributes_of_flags f Attributes.(mk_atts ~polymorphic:poly ()) in
-      let poly = atts.Attributes.polymorphic in
-      static_classifier ~poly e
+      let poly' = Attributes.(parse_drop_extra polymorphic f) in
+      static_classifier ~poly:(Option.default poly poly') e
     | VernacTimeout (_,e) -> static_control_classifier ~poly e
     | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) ->
        static_control_classifier ~poly e
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index c93ff2a63a..b35a4428f9 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -11,6 +11,55 @@
 open CErrors
 open Vernacexpr
 
+let unsupported_attributes ?loc = function
+  | [] -> ()
+  | atts ->
+    let keys = List.map fst atts in
+    let keys = List.sort_uniq String.compare keys in
+    let conj = match keys with [_] -> "this attribute: " | _ -> "these attributes: " in
+    user_err ?loc Pp.(str "This command does not support " ++ str conj ++ prlist str keys ++ str".")
+
+type 'a key_parser = 'a option -> Vernacexpr.vernac_flag_value -> 'a
+
+type 'a attribute = ('a -> Vernacexpr.vernac_flag_value -> 'a) CString.Map.t * 'a
+
+let parse_drop_extra (p,v:'a attribute) (atts:vernac_flags) : 'a =
+  List.fold_left (fun v (k,args) ->
+      match CString.Map.find k p with
+      | exception Not_found -> v
+      | parser -> parser v args)
+    v atts
+
+let parse_with_extra (p,v:'a attribute) (atts:vernac_flags) : 'a * vernac_flags =
+  let v, extra = List.fold_left (fun (v,extra) (k,args as att) ->
+      match CString.Map.find k p with
+      | exception Not_found -> (v,att::extra)
+      | parser -> (parser v args, extra))
+      (v,[]) atts
+  in
+  v, List.rev extra
+
+let parse (p:'a attribute) atts : 'a =
+  let v, extra = parse_with_extra p atts in
+  unsupported_attributes extra;
+  v
+
+module Notations = struct
+
+  let (++) (p1,v1:'a attribute) (p2,v2:'b attribute) : ('a*'b) attribute =
+    let p = CString.Map.merge (fun key p1 p2 -> match p1, p2 with
+        | Some p1, None -> Some (fun (x,y) args -> (p1 x args, y))
+        | None, Some p2 -> Some (fun (x,y) args -> (x, p2 y args))
+        | None, None -> None
+        | Some _, Some _ ->
+          anomaly Pp.(str "Attribute collision on " ++ str key))
+        p1 p2
+    in
+    p, (v1, v2)
+
+end
+open Notations
+
 type deprecation = { since : string option ; note : string option }
 
 let mk_deprecation ?(since=None) ?(note=None) () =
@@ -24,71 +73,62 @@ type t = {
   deprecated : deprecation option;
 }
 
-let default = {
-  locality = None;
-  polymorphic = false;
-  template = None;
-  program = false;
-  deprecated = None;
-}
+let assert_empty k v =
+  if v <> VernacFlagEmpty
+  then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments")
 
-let mk_atts ?(polymorphic=default.polymorphic) ?(program=default.program) () =
-  { default with polymorphic; program }
+let assert_once ~name prev =
+  if Option.has_some prev then
+    user_err Pp.(str "Attribute for " ++ str name ++ str " specified twice.")
 
-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")
+let attribute_of_list (l:(string * 'a key_parser) list) : 'a option attribute =
+  List.fold_left (fun acc (k,p) -> CString.Map.add k (fun prev args -> Some (p prev args)) acc)
+    CString.Map.empty l, None
+
+let single_key_parser ~name ~key v prev args =
+  assert_empty key args;
+  assert_once ~name prev;
+  v
+
+let bool_attribute ~name ~on ~off : bool option attribute =
+  attribute_of_list [(on, single_key_parser ~name ~key:on true);
+               (off, single_key_parser ~name ~key:off false)]
+
+let polymorphic = bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic"
+
+let program = bool_attribute ~name:"Program mode" ~on:"program" ~off:"noprogram"
+
+let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global"
+
+let template = bool_attribute ~name:"Template" ~on:"template" ~off:"notemplate"
+
+let deprecation_parser : deprecation key_parser = fun orig args ->
+  assert_once ~name:"deprecation" orig;
+  match args with
+  | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ]
+  | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] ->
+    let since = Some since and note = Some note in
+    mk_deprecation ~since ~note ()
+  | VernacFlagList [ "since", VernacFlagLeaf since ] ->
+    let since = Some since in
+    mk_deprecation ~since ()
+  | VernacFlagList [ "note", VernacFlagLeaf note ] ->
+    let note = Some note in
+    mk_deprecation ~note ()
+  |  _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute")
+
+let deprecation = attribute_of_list ["deprecated",deprecation_parser]
+
+let attributes_of_flags f =
+  let (((locality, template), deprecated), polymorphic), program =
+    parse (locality ++ template ++ deprecation ++ polymorphic ++ program) f
   in
-  List.fold_left
-    (fun (polymorphism, atts) (k, v) ->
-       match k with
-       | "program" when not atts.program ->
-         assert_empty k v;
-         (polymorphism, { atts with program = true })
-       | "program" ->
-         user_err Pp.(str "Program mode specified twice")
-       | "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")
-       | "template" when atts.template = None ->
-         assert_empty k v;
-         polymorphism, { atts with template = Some true }
-       | "notemplate" when atts.template = None ->
-         assert_empty k v;
-         polymorphism, { atts with template = Some false }
-       | "template" | "notemplate" ->
-         user_err Pp.(str "Templateness specified twice")
-       | "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")
-       | "deprecated" when Option.is_empty atts.deprecated ->
-           begin match v with
-             | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ]
-             | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] ->
-               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" ->
-         user_err Pp.(str "Deprecation specified twice")
-       | _ -> user_err Pp.(str "Unknown attribute " ++ str k)
-    )
-    (None, atts)
-    f
+  let polymorphic = Option.default (Flags.is_universe_polymorphism()) polymorphic in
+  let program = Option.default (Flags.is_program_mode()) program in
+  { polymorphic; program; locality; template; deprecated }
+
+let only_locality atts = parse locality atts
+
+let only_polymorphism atts =
+  let att = parse polymorphic atts in
+  Option.default (Flags.is_universe_polymorphism ()) att
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index b9191c3f3e..5b03c26cb1 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -8,10 +8,34 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Vernacexpr
+
+type 'a attribute
+(** The type of attributes. When parsing attributes if an ['a
+   attribute] is present then an ['a] value will be produced. *)
+
+val parse : 'a attribute -> vernac_flags -> 'a
+(** Errors on unsupported attributes. *)
+
+module Notations : sig
+  (** Notations to combine attributes. *)
+
+  val (++) : 'a attribute -> 'b attribute -> ('a * 'b) attribute
+  (** Combine 2 attributes. If any keys are in common an error will be raised. *)
+end
+
+(** Definitions for some standard attributes. *)
+
 type deprecation = { since : string option ; note : string option }
 
 val mk_deprecation : ?since: string option -> ?note: string option -> unit -> deprecation
 
+val polymorphic : bool option attribute
+val program : bool option attribute
+val template : bool option attribute
+val locality : bool option attribute
+val deprecation : deprecation option attribute
+
 type t = {
   locality : bool option;
   polymorphic : bool;
@@ -19,10 +43,58 @@ type t = {
   program : bool;
   deprecated : deprecation option;
 }
+(** Some attributes gathered in a adhoc record. Will probably be
+   removed at some point. *)
+
+val attributes_of_flags : vernac_flags -> t
+(** Parse the attributes supported by type [t]. Errors on other
+   attributes. Polymorphism and Program use the global flags as
+   default values. *)
+
+val only_locality : vernac_flags -> bool option
+(** Parse attributes allowing only locality. *)
+
+val only_polymorphism : vernac_flags -> bool
+(** Parse attributes allowing only polymorphism.
+    Uses the global flag for the default value. *)
+
+val parse_drop_extra : 'a attribute -> vernac_flags -> 'a
+(** Ignores unsupported attributes. *)
+
+val parse_with_extra : 'a attribute -> vernac_flags -> 'a * vernac_flags
+(** Returns unsupported attributes. *)
+
+(** * Defining attributes. *)
+
+type 'a key_parser = 'a option -> Vernacexpr.vernac_flag_value -> 'a
+(** A parser for some key in an attribute. It is given a nonempty ['a
+    option] when the attribute is multiply set for some command.
+
+    eg in [#[polymorphic] Monomorphic Definition foo := ...], when
+   parsing [Monomorphic] it will be given [Some true]. *)
+
+val attribute_of_list : (string * 'a key_parser) list -> 'a option attribute
+(** Make an attribute from a list of key parsers together with their
+   associated key. *)
+
+val bool_attribute : name:string -> on:string -> off:string -> bool option attribute
+(** Define boolean attribute [name] with value [true] when [on] is
+   provided and [false] when [off] is provided. The attribute may only
+   be set once for a command. *)
+
+(** Combinators to help define your own parsers. See the
+   implementation of [bool_attribute] for practical use. *)
+
+val assert_empty : string -> vernac_flag_value -> unit
+(** [assert_empty key v] errors if [v] is not empty. [key] is used in
+   the error message as the name of the attribute. *)
 
-val mk_atts :
-  ?polymorphic: bool ->
-  ?program: bool -> unit -> t
+val assert_once : name:string -> 'a option -> unit
+(** [assert_once ~name v] errors if [v] is not empty. [name] is used
+   in the error message as the name of the attribute. Used to ensure
+   that a given attribute is not reapeated. *)
 
-val attributes_of_flags : Vernacexpr.vernac_flags -> t ->
-  bool option (* polymorphism attr *) * t
+val single_key_parser : name:string -> key:string -> 'a -> 'a key_parser
+(** [single_key_parser ~name ~key v] makes a parser for attribute
+    [name] giving the constant value [v] for key [key] taking no
+    arguments. [name] may only be given once. *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 12feb07051..b02d482761 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2109,7 +2109,6 @@ let vernac_load interp fname =
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
  * loc is the Loc.t of the vernacular command being interpreted. *)
 let interp ?proof ~atts ~st c =
-  vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
   match c with
 
   (* Loading a file requires access to the control interpreter *)
@@ -2259,11 +2258,7 @@ let interp ?proof ~atts ~st c =
     Option.iter vernac_set_used_variables using
   | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"]
 
-  (* Extensions *)
-  | VernacExtend (opn,args) ->
-    (* XXX: Here we are returning the state! :) *)
-    let _st : Vernacstate.t = Vernacinterp.call ~atts opn args ~st in
-    ()
+  | VernacExtend _ -> assert false
 
 (* Vernaculars that take a locality flag *)
 let check_vernac_supports_locality c l =
@@ -2291,6 +2286,21 @@ let check_vernac_supports_locality c l =
     | VernacInductive _) -> ()
   | Some _, _ -> user_err Pp.(str "This command does not support Locality")
 
+
+let interp  ?proof ~atts ~st c =
+  vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
+  match c with
+  (* Extensions *)
+  | VernacExtend (opn,args) ->
+    (* XXX: Here we are returning the state! :) *)
+    let _st : Vernacstate.t = Vernacinterp.call ~atts opn args ~st in
+    ()
+
+  | _ ->
+    let atts = Attributes.attributes_of_flags atts in
+    check_vernac_supports_locality c atts.locality;
+    interp ?proof ~atts ~st c
+
 (* Vernaculars that take a polymorphism flag *)
 let check_vernac_supports_polymorphism c p =
   match p, c with
@@ -2374,9 +2384,8 @@ 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 rec control = function
-  | VernacExpr (f, v) ->
-    let (polymorphism, atts) = attributes_of_flags f (mk_atts ~program:orig_program_mode ()) in
-    aux ~polymorphism ~atts v
+  | VernacExpr (atts, v) ->
+    aux ~atts v
   | VernacFail v -> with_fail st true (fun () -> control v)
   | VernacTimeout (n,v) ->
     current_timeout := Some n;
@@ -2386,28 +2395,28 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
   | VernacTime (batch, {v}) ->
     System.with_time ~batch control v;
 
-  and aux ~polymorphism ~atts : _ -> unit =
+  and aux ~atts : _ -> unit =
     function
 
     | VernacLoad (_,fname) -> vernac_load control fname
 
     | c ->
-      check_vernac_supports_locality c atts.locality;
-      check_vernac_supports_polymorphism c polymorphism;
-      let polymorphic = Option.default (Flags.is_universe_polymorphism ()) polymorphism in
-      Flags.make_universe_polymorphism polymorphic;
-      Obligations.set_program_mode atts.program;
+      let poly, program = Attributes.(parse_drop_extra Notations.(polymorphic ++ program) atts) in
+      (* NB: we keep polymorphism and program in the attributes, we're
+         just parsing them to do our option magic. *)
+      check_vernac_supports_polymorphism c poly;
+      Option.iter Flags.make_universe_polymorphism poly;
+      Option.iter Obligations.set_program_mode program;
       try
         vernac_timeout begin fun () ->
-          let atts = { atts with polymorphic } in
           if verbosely
           then Flags.verbosely (interp ?proof ~atts ~st) c
           else Flags.silently  (interp ?proof ~atts ~st) c;
           (* If the command is `(Un)Set Program Mode` or `(Un)Set Universe Polymorphism`,
              we should not restore the previous state of the flag... *)
-          if orig_program_mode || not !Flags.program_mode || atts.program then
+          if Option.has_some program then
             Flags.program_mode := orig_program_mode;
-          if (Flags.is_universe_polymorphism() = polymorphic) then
+          if Option.has_some poly then
             Flags.make_universe_polymorphism orig_univ_poly;
           end
         with
@@ -2446,7 +2455,7 @@ open Extend
 type classifier = Genarg.raw_generic_argument list -> vernac_classification
 
 type (_, _) ty_sig =
-| TyNil : (atts:Attributes.t -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
 | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
 | TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
 
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index f95bdaa539..3aa4ec12c0 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -44,7 +44,7 @@ val universe_polymorphism_option_name : string list
 type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification
 
 type (_, _) ty_sig =
-| TyNil : (atts:Attributes.t -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
 | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
 | TyNonTerminal :
   ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig ->
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 27b485d94d..594e9eca48 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -395,7 +395,8 @@ type nonrec vernac_expr =
   (* For extension *)
   | VernacExtend of extend_name * Genarg.raw_generic_argument list
 
-type vernac_flags = (string * vernac_flag_value) list
+type vernac_flags = vernac_flag list
+and vernac_flag = string * vernac_flag_value
 and vernac_flag_value =
   | VernacFlagEmpty
   | VernacFlagLeaf of string
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index b16784eb22..eb4282705e 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -12,7 +12,7 @@ open Util
 open Pp
 open CErrors
 
-type 'a vernac_command = 'a -> atts:Attributes.t -> st:Vernacstate.t -> Vernacstate.t
+type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
 
 type plugin_args = Genarg.raw_generic_argument list
 
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index ba3d911810..0fc02c6915 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -10,7 +10,7 @@
 
 (** Interpretation of extended vernac phrases. *)
 
-type 'a vernac_command = 'a -> atts:Attributes.t -> st:Vernacstate.t -> Vernacstate.t
+type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
 
 type plugin_args = Genarg.raw_generic_argument list
 
@@ -18,4 +18,4 @@ val vinterp_init : unit -> 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:Attributes.t -> st:Vernacstate.t -> Vernacstate.t
+val call : Vernacexpr.extend_name -> plugin_args -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t