Merge PR #8515: Command driven attributes

61 files changed, 1088 insertions, 633 deletions

diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli
index 93a07cff9d..8e10ec49ce 100644
--- a/coqpp/coqpp_ast.mli
+++ b/coqpp/coqpp_ast.mli
@@ -102,6 +102,7 @@ type classification =
 | ClassifName of string
 
 type vernac_rule = {
+  vernac_atts : (string * string) list option;
   vernac_toks : ext_token list;
   vernac_class : code option;
   vernac_depr : bool;
diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll
index cdea4b99ef..c38755943a 100644
--- a/coqpp/coqpp_lex.mll
+++ b/coqpp/coqpp_lex.mll
@@ -130,6 +130,7 @@ rule extend = parse
 | space { extend lexbuf }
 | '\"' { string lexbuf }
 | '\n' { newline lexbuf; extend lexbuf }
+| "#[" { HASHBRACKET }
 | '[' { LBRACKET }
 | ']' { RBRACKET }
 | '|' { PIPE }
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 5314806c24..7cecff9d75 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -309,9 +309,52 @@ let print_rule_classifier fmt r = match r.vernac_class with
   else
     fprintf fmt "Some @[(fun %a-> %a)@]" print_binders r.vernac_toks print_code f
 
+(* let print_atts fmt = function *)
+(*   | None -> fprintf fmt "@[let () = Attributes.unsupported_attributes atts in@] " *)
+(*   | Some atts -> *)
+(*     let rec print_left fmt = function *)
+(*       | [] -> assert false *)
+(*       | [x,_] -> fprintf fmt "%s" x *)
+(*       | (x,_) :: rem -> fprintf fmt "(%s, %a)" x print_left rem *)
+(*     in *)
+(*     let rec print_right fmt = function *)
+(*       | [] -> assert false *)
+(*       | [_,y] -> fprintf fmt "%s" y *)
+(*       | (_,y) :: rem -> fprintf fmt "(%s ++ %a)" y print_right rem *)
+(*     in *)
+(*     let nota = match atts with [_] -> "" | _ -> "Attributes.Notations." in *)
+(*     fprintf fmt "@[let %a = Attributes.parse %s(%a) atts in@] " *)
+(*       print_left atts nota print_right atts *)
+
+let print_atts_left fmt = function
+  | None -> fprintf fmt "()"
+  | Some atts ->
+    let rec aux fmt = function
+      | [] -> assert false
+      | [x,_] -> fprintf fmt "%s" x
+      | (x,_) :: rem -> fprintf fmt "(%s, %a)" x aux rem
+    in
+    aux fmt atts
+
+let print_atts_right fmt = function
+  | None -> fprintf fmt "(Attributes.unsupported_attributes atts)"
+  | Some atts ->
+    let rec aux fmt = function
+      | [] -> assert false
+      | [_,y] -> fprintf fmt "%s" y
+      | (_,y) :: rem -> fprintf fmt "(%s ++ %a)" y aux rem
+    in
+    let nota = match atts with [_] -> "" | _ -> "Attributes.Notations." in
+    fprintf fmt "(Attributes.parse %s%a atts)" nota aux atts
+
+let print_body_fun fmt r =
+  fprintf fmt "let coqpp_body %a%a ~st = let () = %a in st in "
+    print_binders r.vernac_toks print_atts_left r.vernac_atts print_code r.vernac_body
+
 let print_body fmt r =
-  fprintf fmt "@[(fun %a~atts@ ~st@ -> let () = %a in st)@]"
-    print_binders r.vernac_toks print_code r.vernac_body
+  fprintf fmt "@[(%afun %a~atts@ ~st@ -> coqpp_body %a%a ~st)@]"
+    print_body_fun r print_binders r.vernac_toks
+    print_binders r.vernac_toks print_atts_right r.vernac_atts
 
 let rec print_sig fmt = function
 | [] -> fprintf fmt "@[Vernacentries.TyNil@]"
diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly
index 1fb5461b21..abe52ab46b 100644
--- a/coqpp/coqpp_parse.mly
+++ b/coqpp/coqpp_parse.mly
@@ -65,7 +65,7 @@ let parse_user_entry s sep =
 %token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED ARGUMENT
 %token RAW_PRINTED GLOB_PRINTED
 %token COMMAND CLASSIFIED PRINTED TYPED INTERPRETED GLOBALIZED SUBSTITUTED BY AS
-%token LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL STAR
+%token HASHBRACKET LBRACKET RBRACKET PIPE ARROW FUN COMMA EQUAL STAR
 %token LPAREN RPAREN COLON SEMICOLON
 %token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA
 %token EOF
@@ -209,15 +209,32 @@ vernac_rules:
 ;
 
 vernac_rule:
-| PIPE LBRACKET ext_tokens RBRACKET rule_deprecation rule_classifier ARROW CODE
+| PIPE vernac_attributes_opt LBRACKET ext_tokens RBRACKET rule_deprecation rule_classifier ARROW CODE
   { {
-      vernac_toks = $3;
-      vernac_depr = $5;
-      vernac_class= $6;
-      vernac_body = $8;
+      vernac_atts = $2;
+      vernac_toks = $4;
+      vernac_depr = $6;
+      vernac_class= $7;
+      vernac_body = $9;
   } }
 ;
 
+vernac_attributes_opt:
+| { None }
+| HASHBRACKET vernac_attributes RBRACKET { Some $2 }
+;
+
+vernac_attributes:
+| vernac_attribute { [$1] }
+| vernac_attribute SEMICOLON { [$1] }
+| vernac_attribute SEMICOLON vernac_attributes { $1 :: $3 }
+;
+
+vernac_attribute:
+| qualid_or_ident EQUAL qualid_or_ident { ($1, $3) }
+| qualid_or_ident { ($1, $1) }
+;
+
 rule_deprecation:
 | { false }
 | DEPRECATED { true }
diff --git a/dev/ci/user-overlays/08515-command-atts.sh b/dev/ci/user-overlays/08515-command-atts.sh
new file mode 100755
index 0000000000..4605255d5e
--- /dev/null
+++ b/dev/ci/user-overlays/08515-command-atts.sh
@@ -0,0 +1,12 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "8515" ] || [ "$CI_BRANCH" = "command-atts" ]; then
+    ltac2_CI_REF=command-atts
+    ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2
+
+    Equations_CI_REF=command-atts
+    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+    plugin_tutorial_CI_REF=command-atts
+    plugin_tutorial_CI_GITURL=https://github.com/SkySkimmer/plugin_tutorials
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index eb5b9ee1d3..b1fdfafd3a 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -32,6 +32,12 @@ Macros:
 - The RAW_TYPED AS and GLOB_TYPED AS stanzas of the ARGUMENT EXTEND macro are
   deprecated. Use TYPED AS instead.
 
+- coqpp (.mlg) based VERNAC EXTEND accesses attributes through a `#[ x
+  = att ]` syntax, where `att : 'a Attributes.attribute` and `x` will
+  be bound with type `'a` in the expression, unlike the old system
+  where `atts : Vernacexpr.vernac_flags` was bound in the expression
+  and had to be manually parsed.
+
 ## Changes between Coq 8.8 and Coq 8.9
 
 ### ML API
diff --git a/interp/modintern.ml b/interp/modintern.ml
index c27cc9cc07..51e27299e3 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -61,13 +61,52 @@ let lookup_module_or_modtype kind qid =
 
 let lookup_module lqid = fst (lookup_module_or_modtype Module lqid)
 
-let transl_with_decl env = function
+let lookup_polymorphism env base kind fqid =
+  let m = match kind with
+    | Module -> (Environ.lookup_module base env).mod_type
+    | ModType -> (Environ.lookup_modtype base env).mod_type
+    | ModAny -> assert false
+  in
+  let rec defunctor = function
+    | NoFunctor m -> m
+    | MoreFunctor (_,_,m) -> defunctor m
+  in
+  let rec aux m fqid =
+    let open Names in
+    match fqid with
+    | [] -> assert false
+    | [id] ->
+      let test (lab,obj) =
+        match Id.equal (Label.to_id lab) id, obj with
+        | false, _ | _, (SFBmodule _ | SFBmodtype _) -> None
+        | true, SFBmind mind -> Some (Declareops.inductive_is_polymorphic mind)
+        | true, SFBconst const -> Some (Declareops.constant_is_polymorphic const)
+      in
+      (try CList.find_map test m with Not_found -> false (* error later *))
+    | id::rem ->
+      let next = function
+        | MoreFunctor _ -> false (* error later *)
+        | NoFunctor body -> aux body rem
+      in
+      let test (lab,obj) =
+        match Id.equal (Label.to_id lab) id, obj with
+        | false, _ | _, (SFBconst _ | SFBmind _) -> None
+        | true, SFBmodule body -> Some (next body.mod_type)
+        | true, SFBmodtype body ->  (* XXX is this valid? If not error later *)
+          Some (next body.mod_type)
+      in
+      (try CList.find_map test m with Not_found -> false (* error later *))
+  in
+  aux (defunctor m) fqid
+
+let transl_with_decl env base kind = function
   | CWith_Module ({CAst.v=fqid},qid) ->
       WithMod (fqid,lookup_module qid), Univ.ContextSet.empty
   | CWith_Definition ({CAst.v=fqid},udecl,c) ->
     let sigma, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in
     let c, ectx = interp_constr env sigma c in
-    begin match UState.check_univ_decl ~poly:(Flags.is_universe_polymorphism()) ectx udecl with
+    let poly = lookup_polymorphism env base kind fqid in
+    begin match UState.check_univ_decl ~poly ectx udecl with
       | Entries.Polymorphic_const_entry ctx ->
         let inst, ctx = Univ.abstract_universes ctx in
         let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
@@ -86,23 +125,24 @@ let loc_of_module l = l.CAst.loc
 let rec interp_module_ast env kind m cst = match m with
   | {CAst.loc;v=CMident qid} ->
       let (mp,kind) = lookup_module_or_modtype kind qid in
-      (MEident mp, kind, cst)
+      (MEident mp, mp, kind, cst)
   | {CAst.loc;v=CMapply (me1,me2)} ->
-      let me1',kind1, cst = interp_module_ast env kind me1 cst in
-      let me2',kind2, cst = interp_module_ast env ModAny me2 cst in
+      let me1', base, kind1, cst = interp_module_ast env kind me1 cst in
+      let me2', _, kind2, cst = interp_module_ast env ModAny me2 cst in
       let mp2 = match me2' with
         | MEident mp -> mp
         | _ -> error_application_to_not_path (loc_of_module me2) me2'
       in
       if kind2 == ModType then
         error_application_to_module_type (loc_of_module me2);
-      (MEapply (me1',mp2), kind1, cst)
+      (MEapply (me1',mp2), base, kind1, cst)
   | {CAst.loc;v=CMwith (me,decl)} ->
-      let me,kind,cst = interp_module_ast env kind me cst in
+      let me,base,kind,cst = interp_module_ast env kind me cst in
       if kind == Module then error_incorrect_with_in_module m.CAst.loc;
-      let decl, cst' = transl_with_decl env decl in
+      let decl, cst' = transl_with_decl env base kind decl in
       let cst = Univ.ContextSet.union cst cst' in
-      (MEwith(me,decl), kind, cst)
+      (MEwith(me,decl), base, kind, cst)
 
 let interp_module_ast env kind m =
-  interp_module_ast env kind m Univ.ContextSet.empty
+  let me, _, kind, cst = interp_module_ast env kind m Univ.ContextSet.empty in
+  me, kind, cst
diff --git a/lib/flags.ml b/lib/flags.ml
index c8f19f2f11..582506f3a8 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -103,10 +103,6 @@ let auto_intros = ref true
 let make_auto_intros flag = auto_intros := flag
 let is_auto_intros () = !auto_intros
 
-let universe_polymorphism = ref false
-let make_universe_polymorphism b = universe_polymorphism := b
-let is_universe_polymorphism () = !universe_polymorphism
-
 let polymorphic_inductive_cumulativity = ref false
 let make_polymorphic_inductive_cumulativity b = polymorphic_inductive_cumulativity := b
 let is_polymorphic_inductive_cumulativity () = !polymorphic_inductive_cumulativity
diff --git a/lib/flags.mli b/lib/flags.mli
index 3d9eafde75..b667235678 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -84,10 +84,6 @@ val is_auto_intros : unit -> bool
 val program_mode : bool ref
 val is_program_mode : unit -> bool
 
-(** Global universe polymorphism flag. *)
-val make_universe_polymorphism : bool -> unit
-val is_universe_polymorphism : unit -> bool
-
 (** Global polymorphic inductive cumulativity flag. *)
 val make_polymorphic_inductive_cumulativity : bool -> unit
 val is_polymorphic_inductive_cumulativity : unit -> bool
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index c41687e721..b9274cf6b8 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -20,6 +20,7 @@ open Tacticals.New
 open Tacinterp
 open Stdarg
 open Tacarg
+open Attributes
 open Pcoq.Prim
 
 }
@@ -73,10 +74,9 @@ let (set_default_solver, default_solver, print_default_solver) =
 }
 
 VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
-| [ "Set" "Firstorder" "Solver" tactic(t) ] -> {
-    let open Vernacinterp in
+| #[ locality; ] [ "Set" "Firstorder" "Solver" tactic(t) ] -> {
       set_default_solver
-        (Locality.make_section_locality atts.locality)
+        (Locality.make_section_locality locality)
         (Tacintern.glob_tactic t)
   }
 END
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index d4e410bd69..651895aa08 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1004,7 +1004,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
       Ensures by: obvious
       i*)
     (mk_equation_id f_id)
-    (Decl_kinds.Global, Flags.is_universe_polymorphism (), (Decl_kinds.Proof Decl_kinds.Theorem))
+    (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
     evd
   lemma_type
   (Lemmas.mk_hook (fun _ _ -> ()));
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index d57b931785..d1e7d8a5a8 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -307,7 +307,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   begin
     Lemmas.start_proof
       new_princ_name
-      (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem))
+      (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
       !evd
       (EConstr.of_constr new_principle_type)
       hook
@@ -359,10 +359,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
         let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
         let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
         (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
-        let univs =
-          let poly = Flags.is_universe_polymorphism () in
-          Evd.const_univ_entry ~poly evd'
-        in
+        let univs = Evd.const_univ_entry ~poly:false evd' in
         let ce = Declare.definition_entry ~univs value in
         ignore(
 	  Declare.declare_constant
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 7c80b776a4..98aaa081c3 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1494,7 +1494,7 @@ let do_build_inductive
   let _time2 = System.get_time () in
   try
     with_full_print
-      (Flags.silently (ComInductive.do_mutual_inductive ~template:None None rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters))
+      (Flags.silently (ComInductive.do_mutual_inductive ~template:None None rel_inds false false false ~uniform:ComInductive.NonUniformParameters))
       Declarations.Finite
   with
     | UserError(s,msg) as e ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 9a6169d42a..35acbea488 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -414,7 +414,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
       ComDefinition.do_definition
         ~program_mode:false
 	fname
-	(Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl
+        (Decl_kinds.Global,false,Decl_kinds.Definition) pl
 	bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()));
        let evd,rev_pconstants =
 	 List.fold_left
@@ -431,7 +431,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        in
        evd,List.rev rev_pconstants
     | _ ->
-       ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
+       ComFixpoint.do_fixpoint Global false fixpoint_exprl;
        let evd,rev_pconstants =
 	 List.fold_left
            (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 96eb7fbc60..d1a227d517 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -804,7 +804,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
 	 let (typ,_) = lemmas_types_infos.(i) in 
 	 Lemmas.start_proof
 	   lem_id
-	   (Decl_kinds.Global,Flags.is_universe_polymorphism (),((Decl_kinds.Proof Decl_kinds.Theorem)))
+           (Decl_kinds.Global,false,((Decl_kinds.Proof Decl_kinds.Theorem)))
            !evd
 	   typ
            (Lemmas.mk_hook (fun _ _ -> ()));
@@ -866,7 +866,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
 	   i*)
 	 let lem_id = mk_complete_id f_id in
 	 Lemmas.start_proof lem_id
-	   (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma
+           (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) sigma
 	 (fst lemmas_types_infos.(i))
            (Lemmas.mk_hook (fun _ _ -> ()));
 	 ignore (Pfedit.by
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 05a65e4cd8..85fb0c73c9 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -30,7 +30,7 @@ open Namegen
 open Tactypes
 open Tactics
 open Proofview.Notations
-open Vernacinterp
+open Attributes
 
 let wit_hyp = wit_var
 
@@ -321,15 +321,15 @@ 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 }
-| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
+| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] ->
+  { add_rewrite_hint ~poly:polymorphic bl o None l }
+| #[ polymorphic; ] [ "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 }
-| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
-  { add_rewrite_hint ~poly:atts.polymorphic ["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:polymorphic bl o (Some t) l }
+| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] ->
+  { add_rewrite_hint ~poly:polymorphic ["core"] o None l }
+| #[ polymorphic; ] [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] ->
+  { add_rewrite_hint ~poly:polymorphic ["core"] o (Some t) l }
 END
 
 (**********************************************************************)
@@ -411,45 +411,39 @@ let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater
 END*)
 
 VERNAC COMMAND EXTEND DeriveInversionClear
-| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
+| #[ polymorphic; ] [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
   => { seff na }
   -> {
-      let open Vernacinterp in
-      add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_clear_tac }
+      add_inversion_lemma_exn ~poly:polymorphic na c s false inv_clear_tac }
 
-| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => { seff na }
+| #[ polymorphic; ] [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => { seff na }
   -> {
-      let open Vernacinterp in
-      add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_clear_tac }
+      add_inversion_lemma_exn ~poly:polymorphic na c Sorts.InProp false inv_clear_tac }
 END
 
 VERNAC COMMAND EXTEND DeriveInversion
-| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
+| #[ polymorphic; ] [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
   => { seff na }
   -> {
-      let open Vernacinterp in
-      add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_tac }
+      add_inversion_lemma_exn ~poly:polymorphic na c s false inv_tac }
 
-| [ "Derive" "Inversion" ident(na) "with" constr(c) ] => { seff na }
+| #[ polymorphic; ] [ "Derive" "Inversion" ident(na) "with" constr(c) ] => { seff na }
   -> {
-      let open Vernacinterp in
-      add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_tac }
+      add_inversion_lemma_exn ~poly:polymorphic na c Sorts.InProp false inv_tac }
 END
 
 VERNAC COMMAND EXTEND DeriveDependentInversion
-| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
+| #[ polymorphic; ] [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
   => { seff na }
   -> {
-      let open Vernacinterp in
-      add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_tac }
+      add_inversion_lemma_exn ~poly:polymorphic na c s true dinv_tac }
 END
 
 VERNAC COMMAND EXTEND DeriveDependentInversionClear
-| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
+| #[ polymorphic; ] [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
   => { seff na }
   -> {
-      let open Vernacinterp in
-      add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_clear_tac }
+      add_inversion_lemma_exn ~poly:polymorphic na c s true dinv_clear_tac }
 END
 
 (**********************************************************************)
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index c07b653f3a..5af393a3e5 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -239,10 +239,9 @@ ARGUMENT EXTEND opthints
 END
 
 VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
-| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> {
-        let open Vernacinterp in
+| #[ locality = Attributes.locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> {
         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 locality)
           (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 d62f985350..c58c8556c5 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -22,6 +22,7 @@ open Genarg
 open Genredexpr
 open Tok (* necessary for camlp5 *)
 open Names
+open Attributes
 
 open Pcoq
 open Pcoq.Prim
@@ -498,12 +499,12 @@ VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY { pr_ltac_production_item
 END
 
 VERNAC COMMAND EXTEND VernacTacticNotation
-| [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] =>
+| #[ deprecation; locality; ]
+  [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] =>
   { VtSideff [], VtNow } ->
-  { let open Vernacinterp 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
+    Tacentries.add_tactic_notation (Locality.make_module_locality locality) n ?deprecation r e;
   }
 END
 
@@ -545,13 +546,12 @@ PRINTED BY { pr_tacdef_body }
 END
 
 VERNAC COMMAND EXTEND VernacDeclareTacticDefinition
-| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => {
+| #[ deprecation; locality; ] [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => {
     VtSideff (List.map (function
       | TacticDefinition ({CAst.v=r},_) -> r
       | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater
-  } -> { let open Vernacinterp in
-           let deprecation = atts.deprecated in
-           Tacentries.register_ltac (Locality.make_module_locality atts.locality) ?deprecation l;
+  } -> {
+         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 26f2b08d3a..aa78fb5d1e 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -131,10 +131,9 @@ VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF
 END
 
 VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF
-| [ "Obligation" "Tactic" ":=" tactic(t) ] -> {
-        let open Vernacinterp in
+| #[ locality = Attributes.locality; ] [ "Obligation" "Tactic" ":=" tactic(t) ] -> {
         set_default_tactic
-          (Locality.make_section_locality atts.locality)
+          (Locality.make_section_locality locality)
           (Tacintern.glob_tactic t);
   }
 END
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 3e47724c4c..1c7220ddc0 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -180,36 +180,36 @@ TACTIC EXTEND setoid_rewrite
 END
 
 VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF
-  | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
         "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
-      { declare_relation a aeq n (Some lemma1) (Some lemma2) None }
+      { declare_relation atts a aeq n (Some lemma1) (Some lemma2) None }
 
-  | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
         "as" ident(n) ] ->
-      { declare_relation a aeq n (Some lemma1) None None }
-  | [ "Add" "Relation" constr(a) constr(aeq)  "as" ident(n) ] ->
-      { declare_relation a aeq n None None None }
+      { declare_relation atts a aeq n (Some lemma1) None None }
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq)  "as" ident(n) ] ->
+      { declare_relation atts a aeq n None None None }
 END
 
 VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF
-  | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
       "as" ident(n) ] ->
-      { declare_relation a aeq n None (Some lemma2) None }
-  | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
-      { declare_relation a aeq n None (Some lemma2) (Some lemma3) }
+      { declare_relation atts a aeq n None (Some lemma2) None }
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
+      { declare_relation atts a aeq n None (Some lemma2) (Some lemma3) }
 END
 
 VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF
-  | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
-      { declare_relation a aeq n (Some lemma1) None (Some lemma3) }
-  | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+      { declare_relation atts a aeq n (Some lemma1) None (Some lemma3) }
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
       "as" ident(n) ] ->
-      { declare_relation a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
-  | [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
+      { declare_relation atts a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
+  | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
         "as" ident(n) ] ->
-      { declare_relation a aeq n None None (Some lemma3) }
+      { declare_relation atts a aeq n None None (Some lemma3) }
 END
 
 {
@@ -236,64 +236,64 @@ GRAMMAR EXTEND Gram
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF
-  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
         "reflexivity" "proved" "by" constr(lemma1)
         "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
-      { declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) None }
-  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
+      { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) None }
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
         "reflexivity" "proved" "by" constr(lemma1)
         "as" ident(n) ] ->
-      { declare_relation ~binders:b a aeq n (Some lemma1) None None }
-  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)  "as" ident(n) ] ->
-      { declare_relation ~binders:b a aeq n None None None }
+      { declare_relation atts ~binders:b a aeq n (Some lemma1) None None }
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)  "as" ident(n) ] ->
+      { declare_relation atts ~binders:b a aeq n None None None }
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF
-  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
       "as" ident(n) ] ->
-      { declare_relation ~binders:b a aeq n None (Some lemma2) None }
-  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
-      { declare_relation ~binders:b a aeq n None (Some lemma2) (Some lemma3) }
+      { declare_relation atts ~binders:b a aeq n None (Some lemma2) None }
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)  "as" ident(n) ] ->
+      { declare_relation atts ~binders:b a aeq n None (Some lemma2) (Some lemma3) }
 END
 
 VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF
-  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
-      { declare_relation ~binders:b a aeq n (Some lemma1) None (Some lemma3) }
-  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+      { declare_relation atts ~binders:b a aeq n (Some lemma1) None (Some lemma3) }
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
       "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
       "as" ident(n) ] ->
-      { declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
-  | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
+      { declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
         "as" ident(n) ] ->
-      { declare_relation ~binders:b a aeq n None None (Some lemma3) }
+      { declare_relation atts ~binders:b a aeq n None None (Some lemma3) }
 END
 
 VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
-  | [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
-     { let open Vernacinterp in
-         add_setoid (not (Locality.make_section_locality atts.locality)) [] a aeq t n;
+  | #[ atts = rewrite_attributes; ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+     {
+         add_setoid atts [] a aeq t n;
      }
-  | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
-     { let open Vernacinterp in
-         add_setoid (not (Locality.make_section_locality atts.locality)) binders a aeq t n;
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+     {
+         add_setoid atts binders a aeq t n;
      }
-  | [ "Add" "Morphism" constr(m) ":" ident(n) ]
+  | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
     (* This command may or may not open a goal *)
     => { Vernacexpr.VtUnknown, Vernacexpr.VtNow }
-    -> { let open Vernacinterp in
-           add_morphism_infer (not (Locality.make_section_locality atts.locality)) m n;
+    -> {
+           add_morphism_infer atts m n;
        }
-  | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
+  | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
     => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) }
-    -> { let open Vernacinterp in
-           add_morphism (not (Locality.make_section_locality atts.locality)) [] m s n;
+    -> {
+           add_morphism atts [] m s n;
        }
-  | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
+  | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
         "with" "signature" lconstr(s) "as" ident(n) ]
     => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) }
-    -> { let open Vernacinterp in
-           add_morphism (not (Locality.make_section_locality atts.locality)) binders m s n;
+    -> {
+           add_morphism atts binders m s n;
        }
 END
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 8b2721ae4e..7d917c58fe 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -43,6 +43,14 @@ module NamedDecl = Context.Named.Declaration
 
 (** Typeclass-based generalized rewriting. *)
 
+type rewrite_attributes = { polymorphic : bool; program : bool; global : bool }
+
+let rewrite_attributes =
+  let open Attributes.Notations in
+  Attributes.(polymorphic ++ program ++ locality) >>= fun ((polymorphic, program), locality) ->
+  let global = not (Locality.make_section_locality locality) in
+  Attributes.Notations.return { polymorphic; program; global }
+
 (** Constants used by the tactic. *)
 
 let classes_dirpath =
@@ -1776,67 +1784,65 @@ let declare_an_instance n s args =
 
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
-let anew_instance global binders instance fields =
-  let program_mode = Flags.is_program_mode () in
-  let poly = Flags.is_universe_polymorphism () in
-  new_instance ~program_mode poly
+let anew_instance atts binders instance fields =
+  let program_mode = atts.program in
+  new_instance ~program_mode atts.polymorphic
     binders instance (Some (true, CAst.make @@ CRecord (fields)))
-    ~global ~generalize:false ~refine:false Hints.empty_hint_info
+    ~global:atts.global ~generalize:false ~refine:false Hints.empty_hint_info
 
-let declare_instance_refl global binders a aeq n lemma =
+let declare_instance_refl atts binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
-  in anew_instance global binders instance
+  in anew_instance atts binders instance
        [(qualid_of_ident (Id.of_string "reflexivity"),lemma)]
 
-let declare_instance_sym global binders a aeq n lemma =
+let declare_instance_sym atts binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric"
-  in anew_instance global binders instance
+  in anew_instance atts binders instance
        [(qualid_of_ident (Id.of_string "symmetry"),lemma)]
 
-let declare_instance_trans global binders a aeq n lemma =
+let declare_instance_trans atts binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive"
-  in anew_instance global binders instance
+  in anew_instance atts binders instance
        [(qualid_of_ident (Id.of_string "transitivity"),lemma)]
 
-let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
+let declare_relation atts ?(binders=[]) a aeq n refl symm trans =
   init_setoid ();
-  let global = not (Locality.make_section_locality locality) in
   let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation"
-  in ignore(anew_instance global binders instance []);
+  in ignore(anew_instance atts binders instance []);
   match (refl,symm,trans) with
       (None, None, None) -> ()
     | (Some lemma1, None, None) ->
-	ignore (declare_instance_refl global binders a aeq n lemma1)
+        ignore (declare_instance_refl atts binders a aeq n lemma1)
     | (None, Some lemma2, None) ->
-	ignore (declare_instance_sym global binders a aeq n lemma2)
+        ignore (declare_instance_sym atts binders a aeq n lemma2)
     | (None, None, Some lemma3) ->
-	ignore (declare_instance_trans global binders a aeq n lemma3)
+        ignore (declare_instance_trans atts binders a aeq n lemma3)
     | (Some lemma1, Some lemma2, None) ->
-	ignore (declare_instance_refl global binders a aeq n lemma1);
-	ignore (declare_instance_sym global binders a aeq n lemma2)
+        ignore (declare_instance_refl atts binders a aeq n lemma1);
+        ignore (declare_instance_sym atts binders a aeq n lemma2)
     | (Some lemma1, None, Some lemma3) ->
-	let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in
-	let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
+        let _lemma_refl = declare_instance_refl atts binders a aeq n lemma1 in
+        let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder"
 	in ignore(
-	    anew_instance global binders instance
+            anew_instance atts binders instance
               [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1);
                (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)])
     | (None, Some lemma2, Some lemma3) ->
-	let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
-	let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
+        let _lemma_sym = declare_instance_sym atts binders a aeq n lemma2 in
+        let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER"
 	in ignore(
-	    anew_instance global binders instance
+            anew_instance atts binders instance
               [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2);
                (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)])
      | (Some lemma1, Some lemma2, Some lemma3) ->
-	let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in
-	let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
-	let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
+        let _lemma_refl = declare_instance_refl atts binders a aeq n lemma1 in
+        let _lemma_sym = declare_instance_sym atts binders a aeq n lemma2 in
+        let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
 	in ignore(
-	  anew_instance global binders instance
+          anew_instance atts binders instance
             [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1);
              (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2);
              (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)])
@@ -1935,15 +1941,15 @@ let warn_add_setoid_deprecated =
   CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () ->
       Pp.(str "Add Setoid is deprecated, please use Add Parametric Relation."))
 
-let add_setoid global binders a aeq t n =
+let add_setoid atts binders a aeq t n =
   warn_add_setoid_deprecated ?loc:a.CAst.loc ();
   init_setoid ();
-  let _lemma_refl = declare_instance_refl global binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
-  let _lemma_sym = declare_instance_sym global binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
-  let _lemma_trans = declare_instance_trans global binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
+  let _lemma_refl = declare_instance_refl atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
+  let _lemma_sym = declare_instance_sym atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
+  let _lemma_trans = declare_instance_trans atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
   let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
   in ignore(
-    anew_instance global binders instance
+    anew_instance atts binders instance
       [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
        (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
        (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
@@ -1958,26 +1964,26 @@ let warn_add_morphism_deprecated =
   CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
       Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id"))
 
-let add_morphism_infer glob m n =
+let add_morphism_infer atts m n =
   warn_add_morphism_deprecated ?loc:m.CAst.loc ();
   init_setoid ();
-  let poly = Flags.is_universe_polymorphism () in
+  (* NB: atts.program is ignored, program mode automatically set by vernacentries *)
   let instance_id = add_suffix n "_Proper" in
   let env = Global.env () in
   let evd = Evd.from_env env in
   let uctx, instance = build_morphism_signature env evd m in
     if Lib.is_modtype () then
-      let uctx = UState.const_univ_entry ~poly uctx in
+      let uctx = UState.const_univ_entry ~poly:atts.polymorphic uctx in
       let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
 				(Entries.ParameterEntry 
                                  (None,(instance,uctx),None),
 				 Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
 	add_instance (Typeclasses.new_instance 
-                        (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info glob (ConstRef cst));
+                        (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst));
 	declare_projection n instance_id (ConstRef cst)
     else
-      let kind = Decl_kinds.Global, poly, 
+      let kind = Decl_kinds.Global, atts.polymorphic,
 	Decl_kinds.DefinitionBody Decl_kinds.Instance 
       in
       let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
@@ -1985,7 +1991,7 @@ let add_morphism_infer glob m n =
 	| Globnames.ConstRef cst ->
 	  add_instance (Typeclasses.new_instance 
 			  (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
-                          glob (ConstRef cst));
+                          atts.global (ConstRef cst));
 	  declare_projection n instance_id (ConstRef cst)
 	| _ -> assert false
       in
@@ -1995,9 +2001,8 @@ let add_morphism_infer glob m n =
 	    Lemmas.start_proof instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) hook;
 	    ignore (Pfedit.by (Tacinterp.interp tac))) ()
 
-let add_morphism glob binders m s n =
+let add_morphism atts binders m s n =
   init_setoid ();
-  let poly = Flags.is_universe_polymorphism () in
   let instance_id = add_suffix n "_Proper" in
   let instance =
     (((CAst.make @@ Name instance_id),None), Explicit,
@@ -2006,8 +2011,7 @@ let add_morphism glob binders m s n =
 	     [cHole; s; m]))
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
-  let program_mode = Flags.is_program_mode () in
-  ignore(new_instance ~program_mode ~global:glob poly binders instance
+  ignore(new_instance ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance
            (Some (true, CAst.make @@ CRecord []))
     ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
 
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 0d014a0bf3..4f46e78c71 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -19,6 +19,9 @@ open Tacinterp
 
 (** TODO: document and clean me! *)
 
+type rewrite_attributes
+val rewrite_attributes : rewrite_attributes Attributes.attribute
+
 type unary_strategy = 
     Subterms | Subterm | Innermost | Outermost
   | Bottomup | Topdown | Progress | Try | Any | Repeat
@@ -77,18 +80,18 @@ val cl_rewrite_clause :
 val is_applied_rewrite_relation :
   env -> evar_map -> rel_context -> constr -> types option
 
-val declare_relation : ?locality:bool ->
+val declare_relation : rewrite_attributes ->
   ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t ->
   constr_expr option -> constr_expr option -> constr_expr option -> unit
 
 val add_setoid :
-  bool -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr ->
+  rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr ->
   Id.t -> unit
 
-val add_morphism_infer : bool -> constr_expr -> Id.t -> unit
+val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> unit
 
 val add_morphism :
-  bool -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit
+  rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit
 
 val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
 
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 5b4bedb50a..c93d6251e0 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -12,7 +12,7 @@
 
 open Vernacexpr
 open Tacexpr
-open Vernacinterp
+open Attributes
 
 (** {5 Tactic Definitions} *)
 
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index a88285c9ee..d5f22b2c72 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -55,7 +55,7 @@ type alias = KerName.t
 type alias_tactic =
   { alias_args: Id.t list;
     alias_body: glob_tactic_expr;
-    alias_deprecation: Vernacinterp.deprecation option;
+    alias_deprecation: Attributes.deprecation option;
   }
 
 let alias_map = Summary.ref ~name:"tactic-alias"
@@ -121,7 +121,7 @@ type ltac_entry = {
   tac_for_ml : bool;
   tac_body : glob_tactic_expr;
   tac_redef : ModPath.t list;
-  tac_deprecation : Vernacinterp.deprecation option
+  tac_deprecation : Attributes.deprecation option
 }
 
 let mactab =
@@ -178,7 +178,7 @@ let subst_md (subst, (local, id, b, t, deprecation)) =
 let classify_md (local, _, _, _, _ as o) = Substitute o
 
 let inMD : bool * ltac_constant option * bool * glob_tactic_expr *
-           Vernacinterp.deprecation option -> obj =
+           Attributes.deprecation option -> obj =
   declare_object {(default_object "TAC-DEFINITION") with
      cache_function  = cache_md;
      load_function   = load_md;
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index d5d36c97fa..5b98daf383 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -12,7 +12,7 @@ open Names
 open Libnames
 open Tacexpr
 open Geninterp
-open Vernacinterp
+open Attributes
 
 (** This module centralizes the various ways of registering tactics. *)
 
@@ -33,7 +33,7 @@ type alias = KerName.t
 type alias_tactic =
   { alias_args: Id.t list;
     alias_body: glob_tactic_expr;
-    alias_deprecation: Vernacinterp.deprecation option;
+    alias_deprecation: deprecation option;
   }
 (** Contents of a tactic notation *)
 
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 5e2a9af7e5..ebec3c887c 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -122,15 +122,15 @@ let warn_deprecated_tactic =
   CWarnings.create ~name:"deprecated-tactic" ~category:"deprecated"
     (fun (qid,depr) -> str "Tactic " ++ pr_qualid qid ++
       strbrk " is deprecated" ++
-      pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++
-      str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note)
+      pr_opt (fun since -> str "since " ++ str since) depr.Attributes.since ++
+      str "." ++ pr_opt (fun note -> str note) depr.Attributes.note)
 
 let warn_deprecated_alias =
   CWarnings.create ~name:"deprecated-tactic-notation" ~category:"deprecated"
     (fun (kn,depr) -> str "Tactic Notation " ++ Pptactic.pr_alias_key kn ++
       strbrk " is deprecated since" ++
-      pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++
-      str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note)
+      pr_opt (fun since -> str "since " ++ str since) depr.Attributes.since ++
+      str "." ++ pr_opt (fun note -> str note) depr.Attributes.note)
 
 let intern_isolated_global_tactic_reference qid =
   let loc = qid.CAst.loc in
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 940defb743..4ed75cdbe4 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -170,10 +170,9 @@ let declare_one_prenex_implicit locality f =
 }
 
 VERNAC COMMAND EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF
-  | [ "Prenex" "Implicits" ne_global_list(fl) ]
+  | #[ locality = Attributes.locality; ] [ "Prenex" "Implicits" ne_global_list(fl) ]
   -> {
-         let open Vernacinterp in
-         let locality = Locality.make_section_locality atts.locality in
+         let locality = Locality.make_section_locality locality 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 5dbc9eea7a..13e0bcbd47 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 Vernacinterp
 open Ltac_plugin
 open Stdarg
 open Pcoq.Prim
@@ -36,7 +35,7 @@ ARGUMENT EXTEND numnotoption
 END
 
 VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
-  | [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
+  | #[ locality = Attributes.locality; ] [ "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 locality) ty f g (Id.to_string sc) o }
 END
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 4619e049e0..37913edc23 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -227,13 +227,11 @@ let print_if_is_coercion ref =
 let print_polymorphism ref =
   let poly = Global.is_polymorphic ref in
   let template_poly = Global.is_template_polymorphic ref in
-  if Flags.is_universe_polymorphism () || poly || template_poly then
-    [ pr_global ref ++ str " is " ++ str
+  [ pr_global ref ++ str " is " ++ str
       (if poly then "universe polymorphic"
        else if template_poly then
 	 "template universe polymorphic"
        else "not universe polymorphic") ]
-  else []
 
 let print_type_in_type ref =
   let unsafe = Global.is_type_in_type ref in
diff --git a/printing/printer.ml b/printing/printer.ml
index 3cf995a005..da364c8b9e 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -969,19 +969,13 @@ let pr_assumptionset env sigma s =
     ] in
     prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums)
 
-let xor a b = 
-  (a && not b) || (not a && b)
-
 let pr_cumulative poly cum =
   if poly then
     if cum then str "Cumulative " else str "NonCumulative "
   else mt ()
 
 let pr_polymorphic b = 
-  let print = xor (Flags.is_universe_polymorphism ()) b in
-  if print then
-    if b then str"Polymorphic " else str"Monomorphic "
-  else mt ()
+  if b then str"Polymorphic " else str"Monomorphic "
 
 (* print the proof step, possibly with diffs highlighted, *)
 let print_and_diff oldp newp =
diff --git a/stm/stm.ml b/stm/stm.ml
index b731678f6d..514b364af3 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1077,6 +1077,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t
     | _ -> false
   in
   let aux_interp st expr =
+    (* XXX unsupported attributes *)
     let cmd = Vernacprop.under_control expr in
     if is_filtered_command cmd then
       (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st)
@@ -2132,7 +2133,7 @@ and Reach : sig
 end = struct (* {{{ *)
 
 let async_policy () =
-  if Flags.is_universe_polymorphism () then false
+  if Attributes.is_universe_polymorphism () then false
   else if VCS.is_interactive () = `Yes then
     (async_proofs_is_master !cur_opt || !cur_opt.async_proofs_mode = APonLazy)
   else
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 85babd922b..c93487d377 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -50,7 +50,7 @@ let idents_of_name : Names.Name.t -> Names.Id.t list =
 let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"]
 
 let options_affecting_stm_scheduling =
-  [ Vernacentries.universe_polymorphism_option_name;
+  [ Attributes.universe_polymorphism_option_name;
     stm_allow_nested_proofs_option_name ]
 
 let classify_vernac e =
@@ -192,16 +192,15 @@ let classify_vernac e =
         try Vernacentries.get_vernac_classifier s l
         with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
   in
-  let rec static_control_classifier ~poly = function
+  let rec static_control_classifier = function
     | VernacExpr (f, e) ->
-      let _, atts = Vernacentries.attributes_of_flags f Vernacinterp.(mk_atts ~polymorphic:poly ()) in
-      let poly = atts.Vernacinterp.polymorphic in
+      let poly = Attributes.(parse_drop_extra polymorphic_nowarn f) in
       static_classifier ~poly e
-    | VernacTimeout (_,e) -> static_control_classifier ~poly e
+    | VernacTimeout (_,e) -> static_control_classifier e
     | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) ->
-       static_control_classifier ~poly e
+       static_control_classifier e
     | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *)
-        (match static_control_classifier ~poly e with
+        (match static_control_classifier e with
         | ( VtQuery | VtProofStep _ | VtSideff _
           | VtProofMode _ | VtMeta), _ as x -> x
         | VtQed _, _ ->
@@ -209,7 +208,7 @@ let classify_vernac e =
             VtNow
         | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
   in
-  static_control_classifier ~poly:(Flags.is_universe_polymorphism ()) e
+  static_control_classifier e
 
 let classify_as_query = VtQuery, VtLater
 let classify_as_sideeff = VtSideff [], VtLater
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index d587d1f09b..7074ad2d41 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -1,11 +1,13 @@
 Nat.sub : nat -> nat -> nat
 
+Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub but avoid exposing match constructs
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
+Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub when applied to 1 argument
   but avoid exposing match constructs
@@ -13,6 +15,7 @@ Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
+Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub
   when the 1st argument evaluates to a constructor and
@@ -21,6 +24,7 @@ Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
+Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub when the 1st and
   2nd arguments evaluate to a constructor and when applied to 2 arguments 
@@ -28,6 +32,7 @@ Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
+Nat.sub is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 The reduction tactics unfold Nat.sub when the 1st and
   2nd arguments evaluate to a constructor 
@@ -37,6 +42,7 @@ pf :
 forall D1 C1 : Type,
 (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2
 
+pf is not universe polymorphic
 Arguments D2, C2 are implicit
 Arguments D1, C1 are implicit and maximally inserted
 Argument scopes are [foo_scope type_scope _ _ _ _ _]
@@ -45,6 +51,7 @@ pf is transparent
 Expands to: Constant Arguments.pf
 fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
 
+fcomp is not universe polymorphic
 Arguments A, B, C are implicit and maximally inserted
 Argument scopes are [type_scope type_scope type_scope _ _ _]
 The reduction tactics unfold fcomp when applied to 6 arguments 
@@ -52,17 +59,20 @@ fcomp is transparent
 Expands to: Constant Arguments.fcomp
 volatile : nat -> nat
 
+volatile is not universe polymorphic
 Argument scope is [nat_scope]
 The reduction tactics always unfold volatile
 volatile is transparent
 Expands to: Constant Arguments.volatile
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
+f is not universe polymorphic
 Argument scopes are [_ _ nat_scope _ nat_scope]
 f is transparent
 Expands to: Constant Arguments.S1.S2.f
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
+f is not universe polymorphic
 Argument scopes are [_ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 3rd, 4th and
   5th arguments evaluate to a constructor 
@@ -70,6 +80,7 @@ f is transparent
 Expands to: Constant Arguments.S1.S2.f
 f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
+f is not universe polymorphic
 Argument T2 is implicit
 Argument scopes are [type_scope _ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 4th, 5th and
@@ -78,6 +89,7 @@ f is transparent
 Expands to: Constant Arguments.S1.f
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
+f is not universe polymorphic
 Arguments T1, T2 are implicit
 Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope]
 The reduction tactics unfold f when the 5th, 6th and
@@ -90,6 +102,7 @@ Expands to: Constant Arguments.f
      : Prop
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
+f is not universe polymorphic
 The reduction tactics unfold f when the 5th, 6th and
   7th arguments evaluate to a constructor 
 f is transparent
diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out
index febe160820..69ba329ff1 100644
--- a/test-suite/output/ArgumentsScope.out
+++ b/test-suite/output/ArgumentsScope.out
@@ -1,56 +1,70 @@
 a : bool -> bool
 
+a is not universe polymorphic
 Argument scope is [bool_scope]
 Expands to: Variable a
 b : bool -> bool
 
+b is not universe polymorphic
 Argument scope is [bool_scope]
 Expands to: Variable b
 negb'' : bool -> bool
 
+negb'' is not universe polymorphic
 Argument scope is [bool_scope]
 negb'' is transparent
 Expands to: Constant ArgumentsScope.A.B.negb''
 negb' : bool -> bool
 
+negb' is not universe polymorphic
 Argument scope is [bool_scope]
 negb' is transparent
 Expands to: Constant ArgumentsScope.A.negb'
 negb : bool -> bool
 
+negb is not universe polymorphic
 Argument scope is [bool_scope]
 negb is transparent
 Expands to: Constant Coq.Init.Datatypes.negb
 a : bool -> bool
 
+a is not universe polymorphic
 Expands to: Variable a
 b : bool -> bool
 
+b is not universe polymorphic
 Expands to: Variable b
 negb : bool -> bool
 
+negb is not universe polymorphic
 negb is transparent
 Expands to: Constant Coq.Init.Datatypes.negb
 negb' : bool -> bool
 
+negb' is not universe polymorphic
 negb' is transparent
 Expands to: Constant ArgumentsScope.A.negb'
 negb'' : bool -> bool
 
+negb'' is not universe polymorphic
 negb'' is transparent
 Expands to: Constant ArgumentsScope.A.B.negb''
 a : bool -> bool
 
+a is not universe polymorphic
 Expands to: Variable a
 negb : bool -> bool
 
+negb is not universe polymorphic
 negb is transparent
 Expands to: Constant Coq.Init.Datatypes.negb
 negb' : bool -> bool
 
+negb' is not universe polymorphic
 negb' is transparent
 Expands to: Constant ArgumentsScope.negb'
 negb'' : bool -> bool
 
+negb'' is not universe polymorphic
 negb'' is transparent
 Expands to: Constant ArgumentsScope.negb''
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 1755886967..b071da86c9 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -11,7 +11,7 @@ eq_refl
      : ?y = ?y
 where
 ?y : [ |- nat]
-Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+Monomorphic Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
 For eq_refl: Arguments are renamed to B, y
 For eq: Argument A is implicit and maximally inserted
@@ -23,6 +23,7 @@ For eq: Argument scopes are [type_scope _ _]
 For eq_refl: Argument scopes are [type_scope _]
 eq_refl : forall (A : Type) (x : A), x = x
 
+eq_refl is not universe polymorphic
 Arguments are renamed to B, y
 When applied to no arguments:
   Arguments B, y are implicit and maximally inserted
@@ -30,7 +31,8 @@ When applied to 1 argument:
   Argument B is implicit
 Argument scopes are [type_scope _]
 Expands to: Constructor Coq.Init.Logic.eq_refl
-Inductive myEq (B : Type) (x : A) : A -> Prop :=  myrefl : B -> myEq B x x
+Monomorphic Inductive myEq (B : Type) (x : A) : A -> Prop :=
+    myrefl : B -> myEq B x x
 
 For myrefl: Arguments are renamed to C, x, _
 For myrefl: Argument C is implicit and maximally inserted
@@ -38,11 +40,12 @@ For myEq: Argument scopes are [type_scope _ _]
 For myrefl: Argument scopes are [type_scope _ _]
 myrefl : forall (B : Type) (x : A), B -> myEq B x x
 
+myrefl is not universe polymorphic
 Arguments are renamed to C, x, _
 Argument C is implicit and maximally inserted
 Argument scopes are [type_scope _ _]
 Expands to: Constructor Arguments_renaming.Test1.myrefl
-myplus = 
+Monomorphic myplus = 
 fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   match n with
   | 0 => m
@@ -50,11 +53,13 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   end
      : forall T : Type, T -> nat -> nat -> nat
 
+myplus is not universe polymorphic
 Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
 myplus : forall T : Type, T -> nat -> nat -> nat
 
+myplus is not universe polymorphic
 Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
@@ -64,7 +69,7 @@ myplus is transparent
 Expands to: Constant Arguments_renaming.Test1.myplus
 @myplus
      : forall Z : Type, Z -> nat -> nat -> nat
-Inductive myEq (A B : Type) (x : A) : A -> Prop :=
+Monomorphic Inductive myEq (A B : Type) (x : A) : A -> Prop :=
     myrefl : B -> myEq A B x x
 
 For myrefl: Arguments are renamed to A, C, x, _
@@ -73,13 +78,14 @@ For myEq: Argument scopes are [type_scope type_scope _ _]
 For myrefl: Argument scopes are [type_scope type_scope _ _]
 myrefl : forall (A B : Type) (x : A), B -> myEq A B x x
 
+myrefl is not universe polymorphic
 Arguments are renamed to A, C, x, _
 Argument C is implicit and maximally inserted
 Argument scopes are [type_scope type_scope _ _]
 Expands to: Constructor Arguments_renaming.myrefl
 myrefl
      : forall (A C : Type) (x : A), C -> myEq A C x x
-myplus = 
+Monomorphic myplus = 
 fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   match n with
   | 0 => m
@@ -87,11 +93,13 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   end
      : forall T : Type, T -> nat -> nat -> nat
 
+myplus is not universe polymorphic
 Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
 myplus : forall T : Type, T -> nat -> nat -> nat
 
+myplus is not universe polymorphic
 Arguments are renamed to Z, t, n, m
 Argument Z is implicit and maximally inserted
 Argument scopes are [type_scope _ nat_scope nat_scope]
diff --git a/test-suite/output/Binder.out b/test-suite/output/Binder.out
index 34558e9a6b..9c46ace463 100644
--- a/test-suite/output/Binder.out
+++ b/test-suite/output/Binder.out
@@ -1,8 +1,12 @@
-foo = fun '(x, y) => x + y
+Monomorphic foo = fun '(x, y) => x + y
      : nat * nat -> nat
+
+foo is not universe polymorphic
 forall '(a, b), a /\ b
      : Prop
-foo = λ '(x, y), x + y
+Monomorphic foo = λ '(x, y), x + y
      : nat * nat → nat
+
+foo is not universe polymorphic
 ∀ '(a, b), a ∧ b
      : Prop
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index cb835ab48d..0a02c5a7dd 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -1,4 +1,4 @@
-t_rect = 
+Monomorphic t_rect = 
 fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) =>
 fix F (t : t) : P t :=
   match t as t0 return (P t0) with
@@ -7,6 +7,7 @@ fix F (t : t) : P t :=
      : forall P : t -> Type,
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
 
+t_rect is not universe polymorphic
 Argument scopes are [function_scope function_scope _]
      = fun d : TT => match d with
                      | {| f3 := b |} => b
@@ -16,7 +17,7 @@ Argument scopes are [function_scope function_scope _]
                      | {| f3 := b |} => b
                      end
      : TT -> 0 = 0
-proj = 
+Monomorphic proj = 
 fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) =>
 match Nat.eq_dec x y with
 | left eqprf => match eqprf in (_ = z) return (P z) with
@@ -26,8 +27,9 @@ match Nat.eq_dec x y with
 end
      : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
 
+proj is not universe polymorphic
 Argument scopes are [nat_scope nat_scope function_scope _ _]
-foo = 
+Monomorphic foo = 
 fix foo (A : Type) (l : list A) {struct l} : option A :=
   match l with
   | nil => None
@@ -36,17 +38,21 @@ fix foo (A : Type) (l : list A) {struct l} : option A :=
   end
      : forall A : Type, list A -> option A
 
+foo is not universe polymorphic
 Argument scopes are [type_scope list_scope]
-uncast = 
+Monomorphic uncast = 
 fun (A : Type) (x : I A) => match x with
                             | x0 <: _ => x0
                             end
      : forall A : Type, I A -> A
 
+uncast is not universe polymorphic
 Argument scopes are [type_scope _]
-foo' = if A 0 then true else false
+Monomorphic foo' = if A 0 then true else false
      : bool
-f = 
+
+foo' is not universe polymorphic
+Monomorphic f = 
 fun H : B =>
 match H with
 | AC x =>
@@ -56,6 +62,8 @@ match H with
      else fun _ : P false => Logic.I) x
 end
      : B -> True
+
+f is not universe polymorphic
 The command has indeed failed with message:
 Non exhaustive pattern-matching: no clause found for pattern 
 gadtTy _ _
@@ -75,17 +83,22 @@ fun '(D n m p q) => n + m + p + q
      : J -> nat
 The command has indeed failed with message:
 The constructor D (in type J) expects 3 arguments.
-lem1 = 
+Monomorphic lem1 = 
 fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
      : forall k : nat * nat, k = k
-lem2 = 
+
+lem1 is not universe polymorphic
+Monomorphic lem2 = 
 fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl
      : forall k : bool, k = k
 
+lem2 is not universe polymorphic
 Argument scope is [bool_scope]
-lem3 = 
+Monomorphic lem3 = 
 fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
      : forall k : nat * nat, k = k
+
+lem3 is not universe polymorphic
 1 subgoal
   
   x : nat
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 3b65003c29..71c7070f2b 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -2,9 +2,11 @@ compose (C:=nat) S
      : (nat -> nat) -> nat -> nat
 ex_intro (P:=fun _ : nat => True) (x:=0) I
      : ex (fun _ : nat => True)
-d2 = fun x : nat => d1 (y:=x)
+Monomorphic d2 = 
+fun x : nat => d1 (y:=x)
      : forall x x0 : nat, x0 = x -> x0 = x
 
+d2 is not universe polymorphic
 Arguments x, x0 are implicit
 Argument scopes are [nat_scope nat_scope _]
 map id (1 :: nil)
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index af202ea01c..6d65db9e22 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -1,7 +1,8 @@
 The command has indeed failed with message:
 Last occurrence of "list'" must have "A" as 1st argument in
  "A -> list' A -> list' (A * A)%type".
-Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x
+Monomorphic Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=
+    Foo : foo A x
 
 For foo: Argument scopes are [type_scope _]
 For Foo: Argument scopes are [type_scope _]
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index c17c63e724..4743fb0d0a 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -1,4 +1,4 @@
-Inductive sig2 (A : Type) (P Q : A -> Prop) : Type :=
+Monomorphic Inductive sig2 (A : Type) (P Q : A -> Prop) : Type :=
     exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x}
 
 For sig2: Argument A is implicit
diff --git a/test-suite/output/Load.out b/test-suite/output/Load.out
index 0904d5540b..f84cedfa62 100644
--- a/test-suite/output/Load.out
+++ b/test-suite/output/Load.out
@@ -1,6 +1,10 @@
-f = 2
+Monomorphic f = 2
      : nat
-u = I
+
+f is not universe polymorphic
+Monomorphic u = I
      : True
+
+u is not universe polymorphic
 The command has indeed failed with message:
 Files processed by Load cannot leave open proofs.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index d32cf67e28..48379f713d 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -223,13 +223,14 @@ fun S : nat => [[S | S.S]]
      : Set
 exists2 '{{y, z}} : nat * nat, y > z & z > y
      : Prop
-foo = 
+Monomorphic foo = 
 fun l : list nat => match l with
                     | _ :: (_ :: _) as l1 => l1
                     | _ => l
                     end
      : list nat -> list nat
 
+foo is not universe polymorphic
 Argument scope is [list_scope]
 Notation
 "'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index 8a6d94c732..bfeff20524 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -1,20 +1,31 @@
-swap = fun '(x, y) => (y, x)
+Monomorphic swap = fun '(x, y) => (y, x)
      : A * B -> B * A
+
+swap is not universe polymorphic
 fun '(x, y) => (y, x)
      : A * B -> B * A
 forall '(x, y), swap (x, y) = (y, x)
      : Prop
-proj_informative = fun '(exist _ x _) => x : A
+Monomorphic proj_informative = 
+fun '(exist _ x _) => x : A
      : {x : A | P x} -> A
-foo = fun '(Bar n b tt p) => if b then n + p else n - p
+
+proj_informative is not universe polymorphic
+Monomorphic foo = 
+fun '(Bar n b tt p) => if b then n + p else n - p
      : Foo -> nat
-baz = 
+
+foo is not universe polymorphic
+Monomorphic baz = 
 fun '(Bar n1 _ tt p1) '(Bar _ _ tt _) => n1 + p1
      : Foo -> Foo -> nat
-swap = 
+
+baz is not universe polymorphic
+Monomorphic swap = 
 fun (A B : Type) '(x, y) => (y, x)
      : forall A B : Type, A * B -> B * A
 
+swap is not universe polymorphic
 Arguments A, B are implicit and maximally inserted
 Argument scopes are [type_scope type_scope _]
 fun (A B : Type) '(x, y) => swap (x, y) = (y, x)
@@ -29,19 +40,22 @@ exists '(x, y) '(z, w), swap (x, y) = (z, w)
      : A * B → B * A
 ∀ '(x, y), swap (x, y) = (y, x)
      : Prop
-both_z = 
+Monomorphic both_z = 
 fun pat : nat * nat =>
 let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p)
      : forall pat : nat * nat, F pat
+
+both_z is not universe polymorphic
 fun '(x, y) '(z, t) => swap (x, y) = (z, t)
      : A * B -> B * A -> Prop
 forall '(x, y) '(z, t), swap (x, y) = (z, t)
      : Prop
 fun (pat : nat) '(x, y) => x + y = pat
      : nat -> nat * nat -> Prop
-f = fun x : nat => x + x
+Monomorphic f = fun x : nat => x + x
      : nat -> nat
 
+f is not universe polymorphic
 Argument scope is [nat_scope]
 fun x : nat => x + x
      : nat -> nat
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index 38a16e01c2..be793dd453 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -4,7 +4,7 @@ existT is template universe polymorphic
 Argument A is implicit
 Argument scopes are [type_scope function_scope _ _]
 Expands to: Constructor Coq.Init.Specif.existT
-Inductive sigT (A : Type) (P : A -> Type) : Type :=
+Monomorphic Inductive sigT (A : Type) (P : A -> Type) : Type :=
     existT : forall x : A, P x -> {x : A & P x}
 
 For sigT: Argument A is implicit
@@ -14,7 +14,7 @@ For existT: Argument scopes are [type_scope function_scope _ _]
 existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
 
 Argument A is implicit
-Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+Monomorphic Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
 For eq: Argument A is implicit and maximally inserted
 For eq_refl, when applied to no arguments:
@@ -25,6 +25,7 @@ For eq: Argument scopes are [type_scope _ _]
 For eq_refl: Argument scopes are [type_scope _]
 eq_refl : forall (A : Type) (x : A), x = x
 
+eq_refl is not universe polymorphic
 When applied to no arguments:
   Arguments A, x are implicit and maximally inserted
 When applied to 1 argument:
@@ -37,7 +38,7 @@ When applied to no arguments:
   Arguments A, x are implicit and maximally inserted
 When applied to 1 argument:
   Argument A is implicit
-Nat.add = 
+Monomorphic Nat.add = 
 fix add (n m : nat) {struct n} : nat :=
   match n with
   | 0 => m
@@ -45,9 +46,11 @@ fix add (n m : nat) {struct n} : nat :=
   end
      : nat -> nat -> nat
 
+Nat.add is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 Nat.add : nat -> nat -> nat
 
+Nat.add is not universe polymorphic
 Argument scopes are [nat_scope nat_scope]
 Nat.add is transparent
 Expands to: Constant Coq.Init.Nat.add
@@ -55,10 +58,11 @@ Nat.add : nat -> nat -> nat
 
 plus_n_O : forall n : nat, n = n + 0
 
+plus_n_O is not universe polymorphic
 Argument scope is [nat_scope]
 plus_n_O is opaque
 Expands to: Constant Coq.Init.Peano.plus_n_O
-Inductive le (n : nat) : nat -> Prop :=
+Monomorphic Inductive le (n : nat) : nat -> Prop :=
     le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
 
 For le_S: Argument m is implicit
@@ -68,18 +72,21 @@ For le_n: Argument scope is [nat_scope]
 For le_S: Argument scopes are [nat_scope nat_scope _]
 comparison : Set
 
+comparison is not universe polymorphic
 Expands to: Inductive Coq.Init.Datatypes.comparison
-Inductive comparison : Set :=
+Monomorphic Inductive comparison : Set :=
     Eq : comparison | Lt : comparison | Gt : comparison
 bar : foo
 
+bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
 Argument x is implicit and maximally inserted
 Expands to: Constant PrintInfos.bar
-*** [ bar : foo ]
+Monomorphic *** [ bar : foo ]
 
+bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
@@ -87,7 +94,7 @@ Argument x is implicit and maximally inserted
 Module Coq.Init.Peano
 Notation sym_eq := eq_sym
 Expands to: Notation Coq.Init.Logic.sym_eq
-Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
+Monomorphic Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
 For eq: Argument A is implicit and maximally inserted
 For eq_refl, when applied to no arguments:
diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out
index f94ed64234..f080f6d0f0 100644
--- a/test-suite/output/TranspModtype.out
+++ b/test-suite/output/TranspModtype.out
@@ -1,7 +1,15 @@
-TrM.A = M.A
+Monomorphic TrM.A = M.A
      : Set
-OpM.A = M.A
+
+TrM.A is not universe polymorphic
+Monomorphic OpM.A = M.A
      : Set
-TrM.B = M.B
+
+OpM.A is not universe polymorphic
+Monomorphic TrM.B = M.B
      : Set
-*** [ OpM.B : Set ]
+
+TrM.B is not universe polymorphic
+Monomorphic *** [ OpM.B : Set ]
+
+OpM.B is not universe polymorphic
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index acc37f653c..49c292c501 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -1,34 +1,37 @@
-NonCumulative Inductive Empty@{u} : Type@{u} :=  
-NonCumulative Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A }
+Polymorphic NonCumulative Inductive Empty@{u} : Type@{u} :=  
+Polymorphic NonCumulative Record PWrap (A : Type@{u}) : Type@{u} := pwrap
+  { punwrap : A }
 
 PWrap has primitive projections with eta conversion.
 For PWrap: Argument scope is [type_scope]
 For pwrap: Argument scopes are [type_scope _]
-punwrap@{u} = 
+Polymorphic punwrap@{u} = 
 fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p
      : forall A : Type@{u}, PWrap@{u} A -> A
 (* u |=  *)
 
 punwrap is universe polymorphic
 Argument scopes are [type_scope _]
-NonCumulative Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A }
+Polymorphic NonCumulative Record RWrap (A : Type@{u}) : Type@{u} := rwrap
+  { runwrap : A }
 
 For RWrap: Argument scope is [type_scope]
 For rwrap: Argument scopes are [type_scope _]
-runwrap@{u} = 
+Polymorphic runwrap@{u} = 
 fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap
      : forall A : Type@{u}, RWrap@{u} A -> A
 (* u |=  *)
 
 runwrap is universe polymorphic
 Argument scopes are [type_scope _]
-Wrap@{u} = fun A : Type@{u} => A
+Polymorphic Wrap@{u} = 
+fun A : Type@{u} => A
      : Type@{u} -> Type@{u}
 (* u |=  *)
 
 Wrap is universe polymorphic
 Argument scope is [type_scope]
-wrap@{u} = 
+Polymorphic wrap@{u} = 
 fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap
      : forall A : Type@{u}, Wrap@{u} A -> A
 (* u |=  *)
@@ -36,13 +39,13 @@ fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap
 wrap is universe polymorphic
 Arguments A, Wrap are implicit and maximally inserted
 Argument scopes are [type_scope _]
-bar@{u} = nat
+Polymorphic bar@{u} = nat
      : Wrap@{u} Set
 (* u |= Set < u
          *)
 
 bar is universe polymorphic
-foo@{u UnivBinders.17 v} = 
+Polymorphic foo@{u UnivBinders.17 v} = 
 Type@{UnivBinders.17} -> Type@{v} -> Type@{u}
      : Type@{max(u+1,UnivBinders.17+1,v+1)}
 (* u UnivBinders.17 v |=  *)
@@ -75,25 +78,28 @@ mono
      : Type@{mono.u+1}
 The command has indeed failed with message:
 Universe u already exists.
-bobmorane = 
+Monomorphic bobmorane = 
 let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff
      : Type@{max(tt.u,ff.u)}
+
+bobmorane is not universe polymorphic
 The command has indeed failed with message:
 Universe u already bound.
-foo@{E M N} = 
+Polymorphic foo@{E M N} = 
 Type@{M} -> Type@{N} -> Type@{E}
      : Type@{max(E+1,M+1,N+1)}
 (* E M N |=  *)
 
 foo is universe polymorphic
-foo@{u UnivBinders.17 v} = 
+Polymorphic foo@{u UnivBinders.17 v} = 
 Type@{UnivBinders.17} -> Type@{v} -> Type@{u}
      : Type@{max(u+1,UnivBinders.17+1,v+1)}
 (* u UnivBinders.17 v |=  *)
 
 foo is universe polymorphic
-NonCumulative Inductive Empty@{E} : Type@{E} :=  
-NonCumulative Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
+Polymorphic NonCumulative Inductive Empty@{E} : Type@{E} :=  
+Polymorphic NonCumulative Record PWrap (A : Type@{E}) : Type@{E} := pwrap
+  { punwrap : A }
 
 PWrap has primitive projections with eta conversion.
 For PWrap: Argument scope is [type_scope]
@@ -119,45 +125,47 @@ Type@{bind_univs.mono.u}
 (* {bind_univs.mono.u} |=  *)
 
 bind_univs.mono is not universe polymorphic
-bind_univs.poly@{u} = Type@{u}
+Polymorphic bind_univs.poly@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
 
 bind_univs.poly is universe polymorphic
-insec@{v} = Type@{u} -> Type@{v}
+Polymorphic insec@{v} = 
+Type@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* v |=  *)
 
 insec is universe polymorphic
-NonCumulative Inductive insecind@{k} : Type@{k+1} :=
+Polymorphic NonCumulative Inductive insecind@{k} : Type@{k+1} :=
     inseccstr : Type@{k} -> insecind@{k}
 
 For inseccstr: Argument scope is [type_scope]
-insec@{u v} = Type@{u} -> Type@{v}
+Polymorphic insec@{u v} = 
+Type@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
 
 insec is universe polymorphic
-NonCumulative Inductive insecind@{u k} : Type@{k+1} :=
+Polymorphic NonCumulative Inductive insecind@{u k} : Type@{k+1} :=
     inseccstr : Type@{k} -> insecind@{u k}
 
 For inseccstr: Argument scope is [type_scope]
-inmod@{u} = Type@{u}
+Polymorphic inmod@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
 
 inmod is universe polymorphic
-SomeMod.inmod@{u} = Type@{u}
+Polymorphic SomeMod.inmod@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
 
 SomeMod.inmod is universe polymorphic
-inmod@{u} = Type@{u}
+Polymorphic inmod@{u} = Type@{u}
      : Type@{u+1}
 (* u |=  *)
 
 inmod is universe polymorphic
-Applied.infunct@{u v} = 
+Polymorphic Applied.infunct@{u v} = 
 inmod@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out
index 773533a8d3..3dad2360c4 100644
--- a/test-suite/output/goal_output.out
+++ b/test-suite/output/goal_output.out
@@ -1,7 +1,11 @@
-Nat.t = nat
+Monomorphic Nat.t = nat
      : Set
-Nat.t = nat
+
+Nat.t is not universe polymorphic
+Monomorphic Nat.t = nat
      : Set
+
+Nat.t is not universe polymorphic
 1 subgoal
   
   ============================
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index f7ffd1959a..a1326596bb 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -1,9 +1,11 @@
-P = 
+Monomorphic P = 
 fun e : option L => match e with
                     | Some cl => Some cl
                     | None => None
                     end
      : option L -> option L
+
+P is not universe polymorphic
 fun n : nat => let y : T n := A n in ?t ?x : T n
      : forall n : nat, T n
 where
diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v
index 1c6e2d81d8..cfc25c3346 100644
--- a/test-suite/success/Template.v
+++ b/test-suite/success/Template.v
@@ -25,7 +25,7 @@ Module AutoNo.
 End AutoNo.
 
 Module Yes.
-  #[template]
+  #[universes(template)]
   Inductive Box@{i} (A:Type@{i}) : Type@{i} := box : A -> Box A.
 
   About Box.
@@ -37,7 +37,7 @@ Module Yes.
 End Yes.
 
 Module No.
-  #[notemplate]
+  #[universes(notemplate)]
   Inductive Box (A:Type) : Type := box : A -> Box A.
 
   About Box.
diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v
index 7b972f4ed9..f4f59a3c16 100644
--- a/test-suite/success/attribute_syntax.v
+++ b/test-suite/success/attribute_syntax.v
@@ -11,7 +11,7 @@ End Scope.
 
 Fail Check 0 = true :> nat.
 
-#[polymorphic]
+#[universes(polymorphic)]
 Definition ι T (x: T) := x.
 
 Check ι _ ι.
@@ -24,9 +24,9 @@ Reset f.
 Ltac foo := foo.
 
 Module M.
-  #[local] #[polymorphic] Definition zed := Type.
+  #[local] #[universes(polymorphic)] Definition zed := Type.
 
-  #[local, polymorphic] Definition kats := Type.
+  #[local, universes(polymorphic)] Definition kats := Type.
 End M.
 Check M.zed@{_}.
 Fail Check zed.
diff --git a/test-suite/success/module_with_def_univ_poly.v b/test-suite/success/module_with_def_univ_poly.v
new file mode 100644
index 0000000000..a547be4c46
--- /dev/null
+++ b/test-suite/success/module_with_def_univ_poly.v
@@ -0,0 +1,31 @@
+
+(* When doing Module Foo with Definition bar := ..., bar must be
+   generated with the same polymorphism as Foo.bar. *)
+Module Mono.
+  Unset Universe Polymorphism.
+  Module Type T.
+    Parameter foo : Type.
+  End T.
+
+  Module Type F(A:T). End F.
+
+  Set Universe Polymorphism.
+  Module M : T with Definition foo := Type.
+    Monomorphic Definition foo := Type.
+  End M.
+End Mono.
+
+Module Poly.
+  Set Universe Polymorphism.
+
+  Module Type T.
+    Parameter foo@{i|Set < i} : Type@{i}.
+  End T.
+
+  Module Type F(A:T). End F.
+
+  Unset Universe Polymorphism.
+  Module M : T with Definition foo := Set : Type.
+    Polymorphic Definition foo := Set : Type.
+  End M.
+End Poly.
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