Merge PR #8515: Command driven attributes

10 files changed, 573 insertions, 350 deletions

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
new file mode 100644
index 0000000000..88638b295b
--- /dev/null
+++ b/vernac/attributes.ml
@@ -0,0 +1,215 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open CErrors
+open Vernacexpr
+
+let unsupported_attributes = 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 Pp.(str "This command does not support " ++ str conj ++ prlist str keys ++ str".")
+
+type 'a key_parser = 'a option -> vernac_flag_value -> 'a
+
+type 'a attribute = vernac_flags -> vernac_flags * 'a
+
+let parse_with_extra (p:'a attribute) (atts:vernac_flags) : vernac_flags * 'a =
+  p atts
+
+let parse_drop_extra att atts =
+  snd (parse_with_extra att atts)
+
+let parse (p:'a attribute) atts : 'a =
+  let extra, v = parse_with_extra p atts in
+  unsupported_attributes extra;
+  v
+
+let make_attribute x = x
+
+module Notations = struct
+
+  type 'a t = 'a attribute
+
+  let return x = fun atts -> atts, x
+
+  let (>>=) att f =
+    fun atts ->
+      let atts, v = att atts in
+      f v atts
+
+  let (>>) p1 p2 =
+    fun atts ->
+      let atts, () = p1 atts in
+      p2 atts
+
+  let map f att =
+    fun atts ->
+      let atts, v = att atts in
+      atts, f v
+
+  let (++) (p1:'a attribute) (p2:'b attribute) : ('a*'b) attribute =
+    fun atts ->
+      let atts, v1 = p1 atts in
+      let atts, v2 = p2 atts in
+      atts, (v1, v2)
+
+end
+open Notations
+
+type deprecation = { since : string option ; note : string option }
+
+let mk_deprecation ?(since=None) ?(note=None) () =
+  { since ; note }
+
+type t = {
+  locality : bool option;
+  polymorphic : bool;
+  template : bool option;
+  program : bool;
+  deprecated : deprecation option;
+}
+
+let assert_empty k v =
+  if v <> VernacFlagEmpty
+  then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments")
+
+let assert_once ~name prev =
+  if Option.has_some prev then
+    user_err Pp.(str "Attribute for " ++ str name ++ str " specified twice.")
+
+let attribute_of_list (l:(string * 'a key_parser) list) : 'a option attribute =
+  let rec p extra v = function
+    | [] -> List.rev extra, v
+    | (key, attv as att) :: rem ->
+      (match CList.assoc_f String.equal key l with
+       | exception Not_found -> p (att::extra) v rem
+       | parser ->
+         let v = Some (parser v attv) in
+         p extra v rem)
+  in
+  p [] 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 qualify_attribute qual (parser:'a attribute) : 'a attribute =
+  fun atts ->
+    let rec extract extra qualified = function
+      | [] -> List.rev extra, List.flatten (List.rev qualified)
+      | (key,attv) :: rem when String.equal key qual ->
+        (match attv with
+         | VernacFlagEmpty | VernacFlagLeaf _ ->
+           CErrors.user_err ~hdr:"qualified_attribute"
+             Pp.(str "Malformed attribute " ++ str qual ++ str ": attribute list expected.")
+         | VernacFlagList atts ->
+           extract extra (atts::qualified) rem)
+      | att :: rem -> extract (att::extra) qualified rem
+    in
+    let extra, qualified = extract [] [] atts in
+    let rem, v = parser qualified in
+    let extra = if rem = [] then extra else (qual, VernacFlagList rem) :: extra in
+    extra, v
+
+let program_opt = bool_attribute ~name:"Program mode" ~on:"program" ~off:"noprogram"
+
+let program = program_opt >>= function
+  | Some b -> return b
+  | None -> return (Flags.is_program_mode())
+
+let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global"
+
+let warn_unqualified_univ_attr =
+  CWarnings.create ~name:"unqualified-univ-attr" ~category:"deprecated"
+    (fun key -> Pp.(str "Attribute " ++ str key ++
+                    str " should be qualified as \"universes("++str key++str")\"."))
+
+let ukey = "universes"
+let universe_transform ~warn_unqualified : unit attribute =
+  fun atts ->
+    let atts = List.map (fun (key,_ as att) ->
+        match key with
+        | "polymorphic" | "monomorphic"
+        | "template" | "notemplate" ->
+          if warn_unqualified then warn_unqualified_univ_attr key;
+          ukey, VernacFlagList [att]
+        | _ -> att) atts
+    in
+    atts, ()
+
+let universe_polymorphism_option_name = ["Universe"; "Polymorphism"]
+let is_universe_polymorphism =
+  let b = ref false in
+  let _ = let open Goptions in
+    declare_bool_option
+      { optdepr  = false;
+        optname  = "universe polymorphism";
+        optkey   = universe_polymorphism_option_name;
+        optread  = (fun () -> !b);
+        optwrite = ((:=) b) }
+  in
+  fun () -> !b
+
+let polymorphic_base =
+  bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic" >>= function
+  | Some b -> return b
+  | None -> return (is_universe_polymorphism())
+
+let polymorphic_nowarn =
+  universe_transform ~warn_unqualified:false >>
+  qualify_attribute ukey polymorphic_base
+
+let universe_poly_template =
+  let template = bool_attribute ~name:"Template" ~on:"template" ~off:"notemplate" in
+  universe_transform ~warn_unqualified:true >>
+  qualify_attribute ukey (polymorphic_base ++ template)
+
+let polymorphic =
+  universe_transform ~warn_unqualified:true >>
+  qualify_attribute ukey polymorphic_base
+
+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, deprecated), (polymorphic, template)), program =
+    parse (locality ++ deprecation ++ universe_poly_template ++ program) f
+  in
+  { polymorphic; program; locality; template; deprecated }
+
+let only_locality atts = parse locality atts
+
+let only_polymorphism atts = parse polymorphic atts
+
+
+let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmpty]
+let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty]
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
new file mode 100644
index 0000000000..c81082d5ad
--- /dev/null
+++ b/vernac/attributes.mli
@@ -0,0 +1,133 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (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.
+    In the most general case, an attribute transforms the raw flags
+   along with its value. *)
+
+val parse : 'a attribute -> vernac_flags -> 'a
+(** Errors on unsupported attributes. *)
+
+val unsupported_attributes : vernac_flags -> unit
+(** Errors if the list of flags is nonempty. *)
+
+module Notations : sig
+  (** Notations to combine attributes. *)
+
+  include Monad.Def with type 'a t = 'a attribute
+  (** Attributes form a monad. [a1 >>= f] means [f] will be run on the
+     flags transformed by [a1] and using the value produced by [a1].
+      The trivial attribute [return x] does no action on the flags. *)
+
+  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 attribute
+val program : bool attribute
+val universe_poly_template : (bool * bool option) attribute
+val locality : bool option attribute
+val deprecation : deprecation option attribute
+
+val program_opt : bool option attribute
+(** For internal use when messing with the global option. *)
+
+type t = {
+  locality : bool option;
+  polymorphic : bool;
+  template : bool option;
+  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 -> vernac_flags * 'a
+(** 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. *)
+
+val qualify_attribute : string -> 'a attribute -> 'a attribute
+(** [qualified_attribute qual att] treats [#[qual(atts)]] like [att]
+   treats [atts]. *)
+
+(** 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 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 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. *)
+
+val make_attribute : (vernac_flags -> vernac_flags * 'a) -> 'a attribute
+(** Make an attribute using the internal representation, thus with
+   access to the full power of attributes. Unstable. *)
+
+(** Compatibility values for parsing [Polymorphic]. *)
+val vernac_polymorphic_flag : vernac_flag
+val vernac_monomorphic_flag : vernac_flag
+
+(** For the stm, do not use! *)
+
+val polymorphic_nowarn : bool attribute
+(** For internal use, avoid warning if not qualified as eg [universes(polymorphic)]. *)
+val universe_polymorphism_option_name : string list
+val is_universe_polymorphism : unit -> bool
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index d7229d32fe..1d0a5ab0a3 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -112,8 +112,10 @@ GRAMMAR EXTEND Gram
     ]
   ;
   vernac_poly:
-    [ [ 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) }
+    [ [ IDENT "Polymorphic"; v = vernac_aux ->
+        { let (f, v) = v in (Attributes.vernac_polymorphic_flag :: f, v) }
+      | IDENT "Monomorphic"; v = vernac_aux ->
+        { let (f, v) = v in (Attributes.vernac_monomorphic_flag :: f, v) }
       | v = vernac_aux -> { v } ]
     ]
   ;
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index d8cd429e6e..c1343fb592 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -101,13 +101,9 @@ let _ =
 
 (* Util *)
 
-let define id internal ctx c t =
+let define ~poly id internal sigma c t =
   let f = declare_constant ~internal in
-  let univs =
-    if Flags.is_universe_polymorphism ()
-    then Polymorphic_const_entry (Evd.to_universe_context ctx)
-    else Monomorphic_const_entry (Evd.universe_context_set ctx)
-  in
+  let univs = Evd.const_univ_entry ~poly sigma in
   let kn = f id
     (DefinitionEntry
       { const_entry_body = c;
@@ -396,11 +392,17 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
     lnamedepindsort (Evd.from_env env0,[],None)
   in
   let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma ~force_mutual lrecspec in
+  let poly =
+    (* NB: build_mutual_induction_scheme forces nonempty list of mutual inductives
+       (force_mutual is about the generated schemes) *)
+    let _,_,ind,_ = List.hd lnamedepindsort in
+    Global.is_polymorphic (IndRef ind)
+  in
   let declare decl fi lrecref =
     let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in
     let decltype = EConstr.to_constr sigma decltype in
     let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
-    let cst = define fi UserIndividualRequest sigma proof_output (Some decltype) in
+    let cst = define ~poly fi UserIndividualRequest sigma proof_output (Some decltype) in
     ConstRef cst :: lrecref
   in
   let _ = List.fold_right2 declare listdecl lrecnames [] in
@@ -457,10 +459,10 @@ let mk_coq_prod sigma = Evarutil.new_global sigma (Coqlib.lib_ref "core.prod.typ
 let mk_coq_pair sigma = Evarutil.new_global sigma (Coqlib.lib_ref "core.prod.intro")
 
 let build_combined_scheme env schemes =
-  let evdref = ref (Evd.from_env env) in
-  let defs = List.map (fun cst ->
-    let evd, c = Evd.fresh_constant_instance env !evdref cst in
-    evdref := evd; (c, Typeops.type_of_constant_in env c)) schemes in
+  let sigma = Evd.from_env env in
+  let sigma, defs = List.fold_left_map (fun sigma cst ->
+    let sigma, c = Evd.fresh_constant_instance env sigma cst in
+    sigma, (c, Typeops.type_of_constant_in env c)) sigma schemes in
   let find_inductive ty =
     let (ctx, arity) = decompose_prod ty in
     let (_, last) = List.hd ctx in
@@ -478,7 +480,7 @@ let build_combined_scheme env schemes =
   *)
   let inprop =
     let inprop (_,t) =
-      Retyping.get_sort_family_of env !evdref (EConstr.of_constr t)
+      Retyping.get_sort_family_of env sigma (EConstr.of_constr t)
       == Sorts.InProp
     in
     List.for_all inprop defs
@@ -489,10 +491,9 @@ let build_combined_scheme env schemes =
     else (mk_coq_prod, mk_coq_pair)
   in
   (* Number of clauses, including the predicates quantification *)
-  let prods = nb_prod !evdref (EConstr.of_constr t) - (nargs + 1) in
-  let sigma, coqand  = mk_and !evdref in
+  let prods = nb_prod sigma (EConstr.of_constr t) - (nargs + 1) in
+  let sigma, coqand  = mk_and sigma in
   let sigma, coqconj = mk_conj sigma in
-  let () = evdref := sigma in
   let relargs = rel_vect 0 prods in
   let concls = List.rev_map
     (fun (cst, t) ->
@@ -501,15 +502,15 @@ let build_combined_scheme env schemes =
   let concl_bod, concl_typ =
     fold_left'
       (fun (accb, acct) (cst, x) ->
-	mkApp (EConstr.to_constr !evdref coqconj, [| x; acct; cst; accb |]),
-	mkApp (EConstr.to_constr !evdref coqand, [| x; acct |])) concls
+        mkApp (EConstr.to_constr sigma coqconj, [| x; acct; cst; accb |]),
+        mkApp (EConstr.to_constr sigma coqand, [| x; acct |])) concls
   in
   let ctx, _ =
     list_split_rev_at prods
       (List.rev_map (fun (x, y) -> LocalAssum (x, y)) ctx) in
   let typ = List.fold_left (fun d c -> Term.mkProd_wo_LetIn c d) concl_typ ctx in
   let body = it_mkLambda_or_LetIn concl_bod ctx in
-  let sigma = Typing.check env !evdref (EConstr.of_constr body) (EConstr.of_constr typ) in
+  let sigma = Typing.check env sigma (EConstr.of_constr body) (EConstr.of_constr typ) in
   (sigma, body, typ)
 
 let do_combined_scheme name schemes =
@@ -523,7 +524,14 @@ let do_combined_scheme name schemes =
   in
   let sigma,body,typ = build_combined_scheme (Global.env ()) csts in
   let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
-  ignore (define name.v UserIndividualRequest sigma proof_output (Some typ));
+  (* It is possible for the constants to have different universe
+     polymorphism from each other, however that is only when the user
+     manually defined at least one of them (as Scheme would pick the
+     polymorphism of the inductive block). In that case if they want
+     some other polymorphism they can also manually define the
+     combined scheme. *)
+  let poly = Global.is_polymorphic (ConstRef (List.hd csts)) in
+  ignore (define ~poly name.v UserIndividualRequest sigma proof_output (Some typ));
   fixpoint_message None [name.v]
 
 (**********************************************************************)
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 356951b695..30fae756e9 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -1,4 +1,5 @@
 Vernacexpr
+Attributes
 Pvernac
 G_vernac
 G_proofs
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 5eace14cbf..27811f85c4 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -31,6 +31,7 @@ open Redexpr
 open Lemmas
 open Locality
 open Vernacinterp
+open Attributes
 
 module NamedDecl = Context.Named.Declaration
 
@@ -409,44 +410,35 @@ let dump_global r =
 (**********)
 (* Syntax *)
 
-let vernac_syntax_extension ~atts infix l =
-  let local = enforce_module_locality atts.locality in
+let vernac_syntax_extension ~module_local infix l =
   if infix then Metasyntax.check_infix_modifiers (snd l);
-  Metasyntax.add_syntax_extension local l
+  Metasyntax.add_syntax_extension module_local l
 
-let vernac_declare_scope ~atts sc =
-  let local = enforce_module_locality atts.locality in
-  Metasyntax.declare_scope local sc
+let vernac_declare_scope ~module_local sc =
+  Metasyntax.declare_scope module_local sc
 
-let vernac_delimiters ~atts sc action =
-  let local = enforce_module_locality atts.locality in
+let vernac_delimiters ~module_local sc action =
   match action with
-  | Some lr -> Metasyntax.add_delimiters local sc lr
-  | None -> Metasyntax.remove_delimiters local sc
+  | Some lr -> Metasyntax.add_delimiters module_local sc lr
+  | None -> Metasyntax.remove_delimiters module_local sc
 
-let vernac_bind_scope ~atts sc cll =
-  let local = enforce_module_locality atts.locality in
-  Metasyntax.add_class_scope local sc (List.map scope_class_of_qualid cll)
+let vernac_bind_scope ~module_local sc cll =
+  Metasyntax.add_class_scope module_local sc (List.map scope_class_of_qualid cll)
 
-let vernac_open_close_scope ~atts (b,s) =
-  let local = enforce_section_locality atts.locality in
-  Notation.open_close_scope (local,b,s)
+let vernac_open_close_scope ~section_local (b,s) =
+  Notation.open_close_scope (section_local,b,s)
 
-let vernac_arguments_scope ~atts r scl =
-  let local = make_section_locality atts.locality in
-  Notation.declare_arguments_scope local (smart_global r) scl
+let vernac_arguments_scope ~section_local r scl =
+  Notation.declare_arguments_scope section_local (smart_global r) scl
 
-let vernac_infix ~atts =
-  let local = enforce_module_locality atts.locality in
-  Metasyntax.add_infix local (Global.env())
+let vernac_infix ~module_local =
+  Metasyntax.add_infix module_local (Global.env())
 
-let vernac_notation ~atts =
-  let local = enforce_module_locality atts.locality in
-  Metasyntax.add_notation local (Global.env())
+let vernac_notation ~module_local =
+  Metasyntax.add_notation module_local (Global.env())
 
-let vernac_custom_entry ~atts s =
-  let local = enforce_module_locality atts.locality in
-  Metasyntax.declare_custom_entry local s
+let vernac_custom_entry ~module_local s =
+  Metasyntax.declare_custom_entry module_local s
 
 (***********)
 (* Gallina *)
@@ -488,6 +480,7 @@ let vernac_definition_hook p = function
 | _ -> no_hook
 
 let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
+  let atts = attributes_of_flags atts in
   let local = enforce_locality_exp atts.locality discharge in
   let hook = vernac_definition_hook atts.polymorphic kind in
   let () =
@@ -518,6 +511,7 @@ let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
         (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook)
 
 let vernac_start_proof ~atts kind l =
+  let atts = attributes_of_flags atts in
   let local = enforce_locality_exp atts.locality NoDischarge in
   if Dumpglob.dump () then
     List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
@@ -535,6 +529,7 @@ let vernac_exact_proof c =
   if not status then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_assumption ~atts discharge kind l nl =
+  let atts = attributes_of_flags atts in
   let local = enforce_locality_exp atts.locality discharge in
   let global = local == Global in
   let kind = local, atts.polymorphic, kind in
@@ -604,6 +599,7 @@ let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) =
     indicates whether the type is inductive, co-inductive or
     neither. *)
 let vernac_inductive ~atts cum lo finite indl =
+  let atts = attributes_of_flags atts in
   let open Pp in
   let udecl, indl = extract_inductive_udecl indl in
   if Dumpglob.dump () then
@@ -699,6 +695,7 @@ let vernac_inductive ~atts cum lo finite indl =
     *)
 
 let vernac_fixpoint ~atts discharge l =
+  let atts = attributes_of_flags atts in
   let local = enforce_locality_exp atts.locality discharge in
   if Dumpglob.dump () then
     List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
@@ -711,6 +708,7 @@ let vernac_fixpoint ~atts discharge l =
   do_fixpoint local atts.polymorphic l
 
 let vernac_cofixpoint ~atts discharge l =
+  let atts = attributes_of_flags atts in
   let local = enforce_locality_exp atts.locality discharge in
   if Dumpglob.dump () then
     List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
@@ -737,19 +735,19 @@ let vernac_combined_scheme lid l =
      List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ AN (qualid_of_ident ?loc id))) l);
  Indschemes.do_combined_scheme lid l
 
-let vernac_universe ~atts l =
-  if atts.polymorphic && not (Lib.sections_are_opened ()) then
-    user_err ?loc:atts.loc ~hdr:"vernac_universe"
+let vernac_universe ~poly l =
+  if poly && not (Lib.sections_are_opened ()) then
+    user_err ~hdr:"vernac_universe"
 		 (str"Polymorphic universes can only be declared inside sections, " ++
 		  str "use Monomorphic Universe instead");
-  Declare.do_universe atts.polymorphic l
+  Declare.do_universe poly l
 
-let vernac_constraint ~atts l =
-  if atts.polymorphic && not (Lib.sections_are_opened ()) then
-    user_err ?loc:atts.loc ~hdr:"vernac_constraint"
+let vernac_constraint ~poly l =
+  if poly && not (Lib.sections_are_opened ()) then
+    user_err ~hdr:"vernac_constraint"
 		 (str"Polymorphic universe constraints can only be declared"
 		  ++ str " inside sections, use Monomorphic Constraint instead");
-  Declare.do_constraint atts.polymorphic l
+  Declare.do_constraint poly l
 
 (**********************)
 (* Modules            *)
@@ -933,32 +931,35 @@ let vernac_canonical r =
   Recordops.declare_canonical_structure (smart_global r)
 
 let vernac_coercion ~atts ref qids qidt =
-  let local = enforce_locality atts.locality in
+  let local, polymorphic = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
+  let local = enforce_locality local in
   let target = cl_of_qualid qidt in
   let source = cl_of_qualid qids in
   let ref' = smart_global ref in
-  Class.try_add_new_coercion_with_target ref' ~local atts.polymorphic ~source ~target;
+  Class.try_add_new_coercion_with_target ref' ~local polymorphic ~source ~target;
   Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion")
 
 let vernac_identity_coercion ~atts id qids qidt =
-  let local = enforce_locality atts.locality in
+  let local, polymorphic = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
+  let local = enforce_locality local in
   let target = cl_of_qualid qidt in
   let source = cl_of_qualid qids in
-  Class.try_add_new_identity_coercion id ~local atts.polymorphic ~source ~target
+  Class.try_add_new_identity_coercion id ~local polymorphic ~source ~target
 
 (* Type classes *)
 
 let vernac_instance ~atts abst sup inst props pri =
+  let atts = attributes_of_flags atts in
   let global = not (make_section_locality atts.locality) in
   Dumpglob.dump_constraint (fst (pi1 inst)) false "inst";
   let program_mode = Flags.is_program_mode () in
   ignore(Classes.new_instance ~program_mode ~abstract:abst ~global atts.polymorphic sup inst props pri)
 
-let vernac_context ~atts l =
-  if not (Classes.context atts.polymorphic l) then Feedback.feedback Feedback.AddedAxiom
+let vernac_context ~poly l =
+  if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom
 
-let vernac_declare_instances ~atts insts =
-  let glob = not (make_section_locality atts.locality) in
+let vernac_declare_instances ~section_local insts =
+  let glob = not section_local in
   List.iter (fun (id, info) -> Classes.existing_instance glob id (Some info)) insts
 
 let vernac_declare_class id =
@@ -1029,8 +1030,8 @@ let vernac_add_ml_path isrec path =
   let open Mltop in
   add_coq_path { recursive = isrec; path_spec = MlPath (expand path) }
 
-let vernac_declare_ml_module ~atts l =
-  let local = make_locality atts.locality in
+let vernac_declare_ml_module ~local l =
+  let local = Option.default false local in
   Mltop.declare_ml_modules local (List.map expand l)
 
 let vernac_chdir = function
@@ -1062,30 +1063,27 @@ let vernac_restore_state file =
 (************)
 (* Commands *)
 
-let vernac_create_hintdb ~atts id b =
-  let local = make_module_locality atts.locality in
-  Hints.create_hint_db local id full_transparent_state b
+let vernac_create_hintdb ~module_local id b =
+  Hints.create_hint_db module_local id full_transparent_state b
 
-let vernac_remove_hints ~atts dbs ids =
-  let local = make_module_locality atts.locality in
-  Hints.remove_hints local dbs (List.map Smartlocate.global_with_alias ids)
+let vernac_remove_hints ~module_local dbs ids =
+  Hints.remove_hints module_local dbs (List.map Smartlocate.global_with_alias ids)
 
 let vernac_hints ~atts lb h =
-  let local = enforce_module_locality atts.locality in
-  Hints.add_hints ~local lb (Hints.interp_hints atts.polymorphic h)
+  let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
+  let local = enforce_module_locality local in
+  Hints.add_hints ~local lb (Hints.interp_hints poly h)
 
-let vernac_syntactic_definition ~atts lid x y =
+let vernac_syntactic_definition ~module_local lid x y =
   Dumpglob.dump_definition lid false "syndef";
-  let local = enforce_module_locality atts.locality in
-  Metasyntax.add_syntactic_definition (Global.env()) lid.v x local y
+  Metasyntax.add_syntactic_definition (Global.env()) lid.v x module_local y
 
-let vernac_declare_implicits ~atts r l =
-  let local = make_section_locality atts.locality in
+let vernac_declare_implicits ~section_local r l =
   match l with
   | [] ->
-      Impargs.declare_implicits local (smart_global r)
+      Impargs.declare_implicits section_local (smart_global r)
   | _::_ as imps ->
-      Impargs.declare_manual_implicits local (smart_global r) ~enriching:false
+      Impargs.declare_manual_implicits section_local (smart_global r) ~enriching:false
 	(List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps)
 
 let warn_arguments_assert =
@@ -1100,7 +1098,7 @@ let warn_arguments_assert =
 (* [nargs_for_red] is the number of arguments required to trigger reduction,
    [args] is the main list of arguments statuses,
    [more_implicits] is a list of extra lists of implicit statuses  *)
-let vernac_arguments ~atts reference args more_implicits nargs_for_red flags =
+let vernac_arguments ~section_local reference args more_implicits nargs_for_red flags =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let assert_flag = List.mem `Assert flags in
@@ -1311,8 +1309,7 @@ let vernac_arguments ~atts reference args more_implicits nargs_for_red flags =
   (* Actions *)
 
   if renaming_specified then begin
-    let local = make_section_locality atts.locality in
-    Arguments_renaming.rename_arguments local sr names
+    Arguments_renaming.rename_arguments section_local sr names
   end;
 
   if scopes_specified || clear_scopes_flag then begin
@@ -1321,20 +1318,20 @@ let vernac_arguments ~atts reference args more_implicits nargs_for_red flags =
         with UserError _ ->
           Notation.find_delimiters_scope ?loc k)) scopes
       in
-      vernac_arguments_scope ~atts reference scopes
+      vernac_arguments_scope ~section_local reference scopes
     end;
 
   if implicits_specified || clear_implicits_flag then
-    vernac_declare_implicits ~atts reference implicits;
+    vernac_declare_implicits ~section_local reference implicits;
 
   if default_implicits_flag then
-    vernac_declare_implicits ~atts reference [];
+    vernac_declare_implicits ~section_local reference [];
 
   if red_modifiers_specified then begin
     match sr with
     | ConstRef _ as c ->
        Reductionops.ReductionBehaviour.set
-         (make_section_locality atts.locality) c
+         section_local c
          (rargs, Option.default ~-1 nargs_for_red, red_flags)
     | _ -> user_err
              (strbrk "Modifiers of the behavior of the simpl tactic "++
@@ -1362,8 +1359,8 @@ let vernac_reserve bl =
     Reserve.declare_reserved_type idl t)
   in List.iter sb_decl bl
 
-let vernac_generalizable ~atts =
-  let local = make_non_locality atts.locality in
+let vernac_generalizable ~local =
+  let local = Option.default true local in
   Implicit_quantifiers.declare_generalizable ~local
 
 let _ =
@@ -1494,16 +1491,6 @@ let _ =
       optread  = (fun () -> !Flags.program_mode);
       optwrite = (fun b -> Flags.program_mode:=b) }
 
-let universe_polymorphism_option_name = ["Universe"; "Polymorphism"]
-
-let _ =
-  declare_bool_option
-    { optdepr  = false;
-      optname  = "universe polymorphism";
-      optkey   = universe_polymorphism_option_name;
-      optread  = Flags.is_universe_polymorphism;
-      optwrite = Flags.make_universe_polymorphism }
-
 let _ =
   declare_bool_option
     { optdepr  = false;
@@ -1618,8 +1605,8 @@ let _ =
       optread  = Nativenorm.get_profiling_enabled;
       optwrite = Nativenorm.set_profiling_enabled }
 
-let vernac_set_strategy ~atts l =
-  let local = make_locality atts.locality in
+let vernac_set_strategy ~local l =
+  let local = Option.default false local in
   let glob_ref r =
     match smart_global r with
       | ConstRef sp -> EvalConstRef sp
@@ -1629,8 +1616,8 @@ let vernac_set_strategy ~atts l =
   let l = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) l in
   Redexpr.set_strategy local l
 
-let vernac_set_opacity ~atts (v,l) =
-  let local = make_non_locality atts.locality in
+let vernac_set_opacity ~local (v,l) =
+  let local = Option.default true local in
   let glob_ref r =
     match smart_global r with
       | ConstRef sp -> EvalConstRef sp
@@ -1649,8 +1636,8 @@ let get_option_locality export local =
   | Some false -> OptGlobal
   | None -> OptDefault
 
-let vernac_set_option0 ~atts export key opt =
-  let locality = get_option_locality export atts.locality in
+let vernac_set_option0 ~local export key opt =
+  let locality = get_option_locality export local in
   match opt with
   | StringValue s -> set_string_option_value_gen ~locality key s
   | StringOptValue (Some s) -> set_string_option_value_gen ~locality key s
@@ -1658,26 +1645,26 @@ let vernac_set_option0 ~atts export key opt =
   | IntValue n -> set_int_option_value_gen ~locality key n
   | BoolValue b -> set_bool_option_value_gen ~locality key b
 
-let vernac_set_append_option ~atts export key s =
-  let locality = get_option_locality export atts.locality in
+let vernac_set_append_option ~local export key s =
+  let locality = get_option_locality export local in
   set_string_option_append_value_gen ~locality key s
 
-let vernac_set_option ~atts export table v = match v with
+let vernac_set_option ~local export table v = match v with
 | StringValue s ->
   (* We make a special case for warnings because appending is their
   natural semantics *)
   if CString.List.equal table ["Warnings"] then
-    vernac_set_append_option ~atts export table s
+    vernac_set_append_option ~local export table s
   else
     let (last, prefix) = List.sep_last table in
     if String.equal last "Append" && not (List.is_empty prefix) then
-      vernac_set_append_option ~atts export prefix s
+      vernac_set_append_option ~local export prefix s
     else
-      vernac_set_option0 ~atts export table v
-| _ -> vernac_set_option0 ~atts export table v
+      vernac_set_option0 ~local export table v
+| _ -> vernac_set_option0 ~local export table v
 
-let vernac_unset_option ~atts export key =
-  let locality = get_option_locality export atts.locality in
+let vernac_unset_option ~local export key =
+  let locality = get_option_locality export local in
   unset_option_value_gen ~locality key
 
 let vernac_add_option key lv =
@@ -1720,7 +1707,7 @@ let query_command_selector ?loc = function
       (str "Query commands only support the single numbered goal selector.")
 
 let vernac_check_may_eval ~atts redexp glopt rc =
-  let glopt = query_command_selector ?loc:atts.loc glopt in
+  let glopt = query_command_selector glopt in
   let (sigma, env) = get_current_context_of_args glopt in
   let sigma, c = interp_open_constr env sigma rc in
   let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
@@ -1754,8 +1741,8 @@ let vernac_check_may_eval ~atts redexp glopt rc =
   in
   pp ++ Printer.pr_universe_ctx_set sigma uctx
 
-let vernac_declare_reduction ~atts s r =
-  let local = make_locality atts.locality in
+let vernac_declare_reduction ~local s r =
+  let local = Option.default false local in
   let env = Global.env () in
   let sigma = Evd.from_env env in
   declare_red_expr local s (snd (Hook.get f_interp_redexp env sigma r))
@@ -1814,7 +1801,6 @@ let print_about_hyp_globs ?loc ref_or_by_not udecl glopt =
     print_about env sigma ref_or_by_not udecl
 
 let vernac_print ~atts env sigma =
-  let loc = atts.loc in
   function
   | PrintTables -> print_tables ()
   | PrintFullContext-> print_full_context_typ env sigma
@@ -1862,7 +1848,7 @@ let vernac_print ~atts env sigma =
   | PrintVisibility s ->
     Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s
   | PrintAbout (ref_or_by_not,udecl,glnumopt) ->
-    print_about_hyp_globs ?loc ref_or_by_not udecl glnumopt
+    print_about_hyp_globs ref_or_by_not udecl glnumopt
   | PrintImplicit qid ->
     dump_global qid;
     print_impargs qid
@@ -1928,7 +1914,7 @@ let _ =
       optwrite = (:=) search_output_name_only }
 
 let vernac_search ~atts s gopt r =
-  let gopt = query_command_selector ?loc:atts.loc gopt in
+  let gopt = query_command_selector gopt in
   let r = interp_search_restriction r in
   let env,gopt =
     match gopt with | None ->
@@ -2104,12 +2090,25 @@ let vernac_load interp fname =
   if Proof_global.there_are_pending_proofs () then
     CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.")
 
+let with_locality ~atts f =
+  let local = Attributes.(parse locality atts) in
+  f ~local
+
+let with_section_locality ~atts f =
+  let local = Attributes.(parse locality atts) in
+  let section_local = make_section_locality local in
+  f ~section_local
+
+let with_module_locality ~atts f =
+  let local = Attributes.(parse locality atts) in
+  let module_local = make_module_locality local in
+  f ~module_local
+
 (* "locality" is the prefix "Local" attribute, while the "local" component
  * is the outdated/deprecated "Local" attribute of some vernacular commands
  * 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 =
-  let open Vernacinterp in
   vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
   match c with
 
@@ -2133,54 +2132,54 @@ let interp ?proof ~atts ~st c =
 
   (* Syntax *)
   | VernacSyntaxExtension (infix, sl) ->
-      vernac_syntax_extension ~atts infix sl
-  | VernacDeclareScope sc -> vernac_declare_scope ~atts sc
-  | VernacDelimiters (sc,lr) -> vernac_delimiters ~atts sc lr
-  | VernacBindScope (sc,rl) -> vernac_bind_scope ~atts sc rl
-  | VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s)
-  | VernacInfix (mv,qid,sc) -> vernac_infix ~atts mv qid sc
-  | VernacNotation (c,infpl,sc) ->
-      vernac_notation ~atts c infpl sc
+      with_module_locality ~atts vernac_syntax_extension infix sl
+  | VernacDeclareScope sc -> with_module_locality ~atts vernac_declare_scope sc
+  | VernacDelimiters (sc,lr) -> with_module_locality ~atts vernac_delimiters sc lr
+  | VernacBindScope (sc,rl) -> with_module_locality ~atts vernac_bind_scope sc rl
+  | VernacOpenCloseScope (b, s) -> with_section_locality ~atts vernac_open_close_scope (b,s)
+  | VernacInfix (mv,qid,sc) -> with_module_locality ~atts vernac_infix mv qid sc
+  | VernacNotation (c,infpl,sc) -> with_module_locality ~atts vernac_notation c infpl sc
   | VernacNotationAddFormat(n,k,v) ->
-      Metasyntax.add_notation_extra_printing_rule n k v
+    unsupported_attributes atts;
+    Metasyntax.add_notation_extra_printing_rule n k v
   | VernacDeclareCustomEntry s ->
-      vernac_custom_entry ~atts s
+      with_module_locality ~atts vernac_custom_entry s
 
   (* Gallina *)
   | VernacDefinition ((discharge,kind),lid,d) ->
       vernac_definition ~atts discharge kind lid d
   | VernacStartTheoremProof (k,l) -> vernac_start_proof ~atts k l
-  | VernacEndProof e -> vernac_end_proof ?proof e
-  | VernacExactProof c -> vernac_exact_proof c
+  | VernacEndProof e -> unsupported_attributes atts; vernac_end_proof ?proof e
+  | VernacExactProof c -> unsupported_attributes atts; vernac_exact_proof c
   | VernacAssumption ((discharge,kind),nl,l) ->
       vernac_assumption ~atts discharge kind l nl
   | VernacInductive (cum, priv, finite, l) -> vernac_inductive ~atts cum priv finite l
   | VernacFixpoint (discharge, l) -> vernac_fixpoint ~atts discharge l
   | VernacCoFixpoint (discharge, l) -> vernac_cofixpoint ~atts discharge l
-  | VernacScheme l -> vernac_scheme l
-  | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
-  | VernacUniverse l -> vernac_universe ~atts l
-  | VernacConstraint l -> vernac_constraint ~atts l
+  | VernacScheme l -> unsupported_attributes atts; vernac_scheme l
+  | VernacCombinedScheme (id, l) -> unsupported_attributes atts; vernac_combined_scheme id l
+  | VernacUniverse l -> vernac_universe ~poly:(only_polymorphism atts) l
+  | VernacConstraint l -> vernac_constraint ~poly:(only_polymorphism atts) l
 
   (* Modules *)
   | VernacDeclareModule (export,lid,bl,mtyo) ->
-      vernac_declare_module export lid bl mtyo
+      unsupported_attributes atts; vernac_declare_module export lid bl mtyo
   | VernacDefineModule (export,lid,bl,mtys,mexprl) ->
-      vernac_define_module export lid bl mtys mexprl
+      unsupported_attributes atts; vernac_define_module export lid bl mtys mexprl
   | VernacDeclareModuleType (lid,bl,mtys,mtyo) ->
-      vernac_declare_module_type lid bl mtys mtyo
+      unsupported_attributes atts; vernac_declare_module_type lid bl mtys mtyo
   | VernacInclude in_asts ->
-      vernac_include in_asts
+      unsupported_attributes atts; vernac_include in_asts
   (* Gallina extensions *)
-  | VernacBeginSection lid -> vernac_begin_section lid
+  | VernacBeginSection lid -> unsupported_attributes atts; vernac_begin_section lid
 
-  | VernacEndSegment lid -> vernac_end_segment lid
+  | VernacEndSegment lid -> unsupported_attributes atts; vernac_end_segment lid
 
-  | VernacNameSectionHypSet (lid, set) -> vernac_name_sec_hyp lid set
+  | VernacNameSectionHypSet (lid, set) -> unsupported_attributes atts; vernac_name_sec_hyp lid set
 
-  | VernacRequire (from, export, qidl) -> vernac_require from export qidl
-  | VernacImport (export,qidl) -> vernac_import export qidl
-  | VernacCanonical qid -> vernac_canonical qid
+  | VernacRequire (from, export, qidl) -> unsupported_attributes atts; vernac_require from export qidl
+  | VernacImport (export,qidl) -> unsupported_attributes atts; vernac_import export qidl
+  | VernacCanonical qid -> unsupported_attributes atts; vernac_canonical qid
   | VernacCoercion (r,s,t) -> vernac_coercion ~atts r s t
   | VernacIdentityCoercion ({v=id},s,t) ->
       vernac_identity_coercion ~atts id s t
@@ -2188,77 +2187,82 @@ let interp ?proof ~atts ~st c =
   (* Type classes *)
   | VernacInstance (abst, sup, inst, props, info) ->
       vernac_instance ~atts abst sup inst props info
-  | VernacContext sup -> vernac_context ~atts sup
-  | VernacDeclareInstances insts -> vernac_declare_instances ~atts insts
-  | VernacDeclareClass id -> vernac_declare_class id
+  | VernacContext sup -> vernac_context ~poly:(only_polymorphism atts) sup
+  | VernacDeclareInstances insts -> with_section_locality ~atts vernac_declare_instances insts
+  | VernacDeclareClass id -> unsupported_attributes atts; vernac_declare_class id
 
   (* Solving *)
-  | VernacSolveExistential (n,c) -> vernac_solve_existential n c
+  | VernacSolveExistential (n,c) -> unsupported_attributes atts; vernac_solve_existential n c
 
   (* Auxiliary file and library management *)
-  | VernacAddLoadPath (isrec,s,alias) -> vernac_add_loadpath isrec s alias
-  | VernacRemoveLoadPath s -> vernac_remove_loadpath s
-  | VernacAddMLPath (isrec,s) -> vernac_add_ml_path isrec s
-  | VernacDeclareMLModule l -> vernac_declare_ml_module ~atts l
-  | VernacChdir s -> vernac_chdir s
+  | VernacAddLoadPath (isrec,s,alias) -> unsupported_attributes atts; vernac_add_loadpath isrec s alias
+  | VernacRemoveLoadPath s -> unsupported_attributes atts; vernac_remove_loadpath s
+  | VernacAddMLPath (isrec,s) -> unsupported_attributes atts; vernac_add_ml_path isrec s
+  | VernacDeclareMLModule l -> with_locality ~atts vernac_declare_ml_module l
+  | VernacChdir s -> unsupported_attributes atts; vernac_chdir s
 
   (* State management *)
-  | VernacWriteState s -> vernac_write_state s
-  | VernacRestoreState s -> vernac_restore_state s
+  | VernacWriteState s -> unsupported_attributes atts; vernac_write_state s
+  | VernacRestoreState s -> unsupported_attributes atts; vernac_restore_state s
 
   (* Commands *)
-  | VernacCreateHintDb (dbname,b) -> vernac_create_hintdb ~atts dbname b
-  | VernacRemoveHints (dbnames,ids) -> vernac_remove_hints ~atts dbnames ids
+  | VernacCreateHintDb (dbname,b) ->
+    with_module_locality ~atts vernac_create_hintdb dbname b
+  | VernacRemoveHints (dbnames,ids) ->
+    with_module_locality ~atts vernac_remove_hints dbnames ids
   | VernacHints (dbnames,hints) ->
       vernac_hints ~atts dbnames hints
   | VernacSyntacticDefinition (id,c,b) ->
-      vernac_syntactic_definition ~atts id c b
+      with_module_locality ~atts vernac_syntactic_definition id c b
   | VernacArguments (qid, args, more_implicits, nargs, flags) ->
-      vernac_arguments ~atts qid args more_implicits nargs flags
-  | VernacReserve bl -> vernac_reserve bl
-  | VernacGeneralizable gen -> vernac_generalizable ~atts gen
-  | VernacSetOpacity qidl -> vernac_set_opacity ~atts qidl
-  | VernacSetStrategy l -> vernac_set_strategy ~atts l
-  | VernacSetOption (export, key,v) -> vernac_set_option ~atts export key v
-  | VernacUnsetOption (export, key) -> vernac_unset_option ~atts export key
-  | VernacRemoveOption (key,v) -> vernac_remove_option key v
-  | VernacAddOption (key,v) -> vernac_add_option key v
-  | VernacMemOption (key,v) -> vernac_mem_option key v
-  | VernacPrintOption key -> vernac_print_option key
+      with_section_locality ~atts vernac_arguments qid args more_implicits nargs flags
+  | VernacReserve bl -> unsupported_attributes atts; vernac_reserve bl
+  | VernacGeneralizable gen -> with_locality ~atts vernac_generalizable gen
+  | VernacSetOpacity qidl -> with_locality ~atts vernac_set_opacity qidl
+  | VernacSetStrategy l -> with_locality ~atts vernac_set_strategy l
+  | VernacSetOption (export, key,v) -> vernac_set_option ~local:(only_locality atts) export key v
+  | VernacUnsetOption (export, key) -> vernac_unset_option ~local:(only_locality atts) export key
+  | VernacRemoveOption (key,v) -> unsupported_attributes atts; vernac_remove_option key v
+  | VernacAddOption (key,v) -> unsupported_attributes atts; vernac_add_option key v
+  | VernacMemOption (key,v) -> unsupported_attributes atts; vernac_mem_option key v
+  | VernacPrintOption key -> unsupported_attributes atts; vernac_print_option key
   | VernacCheckMayEval (r,g,c) ->
     Feedback.msg_notice @@ vernac_check_may_eval ~atts r g c
-  | VernacDeclareReduction (s,r) -> vernac_declare_reduction ~atts s r
+  | VernacDeclareReduction (s,r) -> with_locality ~atts vernac_declare_reduction s r
   | VernacGlobalCheck c ->
+    unsupported_attributes atts;
     Feedback.msg_notice @@ vernac_global_check c
   | VernacPrint p ->
     let sigma, env = Pfedit.get_current_context () in
     Feedback.msg_notice @@ vernac_print ~atts env sigma p
-  | VernacSearch (s,g,r) -> vernac_search ~atts s g r
-  | VernacLocate l ->
+  | VernacSearch (s,g,r) -> unsupported_attributes atts; vernac_search ~atts s g r
+  | VernacLocate l -> unsupported_attributes atts;
     Feedback.msg_notice @@ vernac_locate l
-  | VernacRegister (qid, r) -> vernac_register qid r
-  | VernacComments l -> Flags.if_verbose Feedback.msg_info (str "Comments ok\n")
+  | VernacRegister (qid, r) -> unsupported_attributes atts; vernac_register qid r
+  | VernacComments l -> unsupported_attributes atts;
+    Flags.if_verbose Feedback.msg_info (str "Comments ok\n")
 
   (* Proof management *)
-  | VernacFocus n -> vernac_focus n
-  | VernacUnfocus -> vernac_unfocus ()
-  | VernacUnfocused ->
+  | VernacFocus n -> unsupported_attributes atts; vernac_focus n
+  | VernacUnfocus -> unsupported_attributes atts; vernac_unfocus ()
+  | VernacUnfocused -> unsupported_attributes atts;
     Feedback.msg_notice @@ vernac_unfocused ()
-  | VernacBullet b -> vernac_bullet b
-  | VernacSubproof n -> vernac_subproof n
-  | VernacEndSubproof -> vernac_end_subproof ()
-  | VernacShow s ->
+  | VernacBullet b -> unsupported_attributes atts; vernac_bullet b
+  | VernacSubproof n -> unsupported_attributes atts; vernac_subproof n
+  | VernacEndSubproof -> unsupported_attributes atts; vernac_end_subproof ()
+  | VernacShow s -> unsupported_attributes atts;
     Feedback.msg_notice @@ vernac_show s
-  | VernacCheckGuard ->
+  | VernacCheckGuard -> unsupported_attributes atts;
     Feedback.msg_notice @@ vernac_check_guard ()
-  | VernacProof (tac, using) ->
+  | VernacProof (tac, using) -> unsupported_attributes atts;
     let using = Option.append using (Proof_using.get_default_proof_using ()) in
     let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in
     let usings = if Option.is_empty using then "using:no" else "using:yes" in
-    Aux_file.record_in_aux_at ?loc:atts.loc "VernacProof" (tacs^" "^usings);
+    Aux_file.record_in_aux_at "VernacProof" (tacs^" "^usings);
     Option.iter vernac_set_end_tac tac;
     Option.iter vernac_set_used_variables using
-  | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"]
+  | VernacProofMode mn -> unsupported_attributes atts;
+    Proof_global.set_proof_mode mn [@ocaml.warning "-3"]
 
   (* Extensions *)
   | VernacExtend (opn,args) ->
@@ -2266,46 +2270,6 @@ let interp ?proof ~atts ~st c =
     let _st : Vernacstate.t = Vernacinterp.call ~atts opn args ~st in
     ()
 
-(* Vernaculars that take a locality flag *)
-let check_vernac_supports_locality c l =
-  match l, c with
-  | None, _ -> ()
-  | Some _, (
-      VernacOpenCloseScope _
-    | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _
-    | VernacDeclareScope _ | VernacDelimiters _ | VernacBindScope _
-    | VernacDeclareCustomEntry _
-    | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _
-    | VernacAssumption _ | VernacStartTheoremProof _
-    | VernacCoercion _ | VernacIdentityCoercion _
-    | VernacInstance _ | VernacDeclareInstances _
-    | VernacDeclareMLModule _
-    | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
-    | VernacSyntacticDefinition _
-    | VernacArguments _
-    | VernacGeneralizable _
-    | VernacSetOpacity _ | VernacSetStrategy _
-    | VernacSetOption _ | VernacUnsetOption _
-    | VernacDeclareReduction _
-    | VernacExtend _ 
-    | VernacRegister _
-    | VernacInductive _) -> ()
-  | Some _, _ -> user_err Pp.(str "This command does not support Locality")
-
-(* Vernaculars that take a polymorphism flag *)
-let check_vernac_supports_polymorphism c p =
-  match p, c with
-  | None, _ -> ()
-  | Some _, (
-      VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _
-    | VernacAssumption _ | VernacInductive _
-    | VernacStartTheoremProof _
-    | VernacCoercion _ | VernacIdentityCoercion _
-    | VernacInstance _ | VernacDeclareInstances _
-    | VernacHints _ | VernacContext _
-    | VernacExtend _ | VernacUniverse _ | VernacConstraint _) -> ()
-  | Some _, _ -> user_err Pp.(str "This command does not support Polymorphism")
-
 (** A global default timeout, controlled by option "Set Default Timeout n".
     Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
 
@@ -2371,71 +2335,11 @@ let with_fail st b f =
       | _ -> assert false
   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) (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 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;
@@ -2445,29 +2349,29 @@ 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
+    | VernacLoad (_,fname) ->
+      unsupported_attributes atts;
+      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 program = let open Attributes in
+        parse_drop_extra program_opt atts
+      in
+      (* NB: we keep polymorphism and program in the attributes, we're
+         just parsing them to do our option magic. *)
+      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
-            Flags.make_universe_polymorphism orig_univ_poly;
           end
         with
         | reraise when
@@ -2478,7 +2382,6 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
             let e = CErrors.push reraise in
             let e = locate_if_not_already ?loc e in
             let () = restore_timeout () in
-            Flags.make_universe_polymorphism orig_univ_poly;
             Flags.program_mode := orig_program_mode;
             iraise e
   in
@@ -2505,7 +2408,7 @@ open Extend
 type classifier = Genarg.raw_generic_argument list -> vernac_classification
 
 type (_, _) ty_sig =
-| TyNil : (atts:atts -> 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 0c4630e45f..8ccd121b8f 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -37,18 +37,12 @@ val command_focus : unit Proof.focus_kind
 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_flags -> Vernacinterp.atts -> bool option * Vernacinterp.atts
-
 (** {5 VERNAC EXTEND} *)
 
 type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification
 
 type (_, _) ty_sig =
-| TyNil : (atts:Vernacinterp.atts -> 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 2746cbd144..eb4282705e 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -12,24 +12,7 @@ open Util
 open Pp
 open CErrors
 
-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;
-  template : bool option;
-  program : bool;
-  deprecated : deprecation option;
-}
-
-let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(template=None) ?(program=false) ?(deprecated=None) () : atts =
-  { loc ; locality ; polymorphic ; program ; deprecated; template }
-
-type 'a vernac_command = 'a -> atts:atts -> 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 62a178b555..0fc02c6915 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -10,24 +10,7 @@
 
 (** Interpretation of extended vernac phrases. *)
 
-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;
-  template : bool option;
-  program : bool;
-  deprecated : deprecation option;
-}
-
-val mk_atts : ?loc: Loc.t option -> ?locality: bool option ->
-  ?polymorphic: bool -> ?template:bool option ->
-  ?program: bool -> ?deprecated: deprecation option -> unit -> atts
-
-type 'a vernac_command = 'a -> atts:atts -> 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
 
@@ -35,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:atts -> st:Vernacstate.t -> Vernacstate.t
+val call : Vernacexpr.extend_name -> plugin_args -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t