Merge PR #8917: Small cleanup wrt attributes_of_flags and template attribute

3 files changed, 35 insertions, 41 deletions

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 75ca027332..4f238f38e6 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -78,14 +78,6 @@ 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")
@@ -181,10 +173,9 @@ 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
+let template =
   universe_transform ~warn_unqualified:true >>
-  qualify_attribute ukey (polymorphic_base ++ template)
+  qualify_attribute ukey (bool_attribute ~name:"Template" ~on:"template" ~off:"notemplate")
 
 let polymorphic =
   universe_transform ~warn_unqualified:true >>
@@ -207,12 +198,6 @@ let deprecation_parser : deprecation key_parser = fun orig args ->
 
 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
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index c2dde4cbcc..6a32960a9d 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -49,28 +49,13 @@ val mk_deprecation : ?since: string option -> ?note: string option -> unit -> de
 
 val polymorphic : bool attribute
 val program : bool attribute
-val universe_poly_template : (bool * bool option) attribute
+val template : 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. *)
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 632df20592..f5d68a2199 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -52,6 +52,23 @@ let cl_of_qualid = function
 let scope_class_of_qualid qid =
   Notation.scope_class_of_class (cl_of_qualid qid)
 
+(** Standard attributes for definition-like commands. *)
+module DefAttributes = struct
+  type t = {
+    locality : bool option;
+    polymorphic : bool;
+    program : bool;
+    deprecated : deprecation option;
+  }
+
+  let parse f =
+    let open Attributes in
+    let ((locality, deprecated), polymorphic), program =
+      parse Notations.(locality ++ deprecation ++ polymorphic ++ program) f
+    in
+    { polymorphic; program; locality; deprecated }
+end
+
 (*******************)
 (* "Show" commands *)
 
@@ -509,7 +526,8 @@ let vernac_definition_hook p = function
 | _ -> None
 
 let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def =
-  let atts = attributes_of_flags atts in
+  let open DefAttributes in
+  let atts = parse atts in
   let local = enforce_locality_exp atts.locality discharge in
   let hook = vernac_definition_hook atts.polymorphic kind in
   let () =
@@ -540,7 +558,8 @@ 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 open DefAttributes in
+  let atts = parse 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;
@@ -558,7 +577,8 @@ 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 open DefAttributes in
+  let atts = parse atts in
   let local = enforce_locality_exp atts.locality discharge in
   let global = local == Global in
   let kind = local, atts.polymorphic, kind in
@@ -633,7 +653,9 @@ 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 DefAttributes in
+  let atts, template = Attributes.(parse_with_extra template atts) in
+  let atts = parse atts in
   let open Pp in
   let udecl, indl = extract_inductive_udecl indl in
   if Dumpglob.dump () then
@@ -658,7 +680,6 @@ let vernac_inductive ~atts cum lo finite indl =
   | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> Some (id, bl, c, l)
   | _ -> None
   in
-  let template = atts.template in
   if Option.has_some is_defclass then
     (** Definitional class case *)
     let (id, bl, c, l) = Option.get is_defclass in
@@ -729,7 +750,8 @@ let vernac_inductive ~atts cum lo finite indl =
     *)
 
 let vernac_fixpoint ~atts discharge l =
-  let atts = attributes_of_flags atts in
+  let open DefAttributes in
+  let atts = parse 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;
@@ -742,7 +764,8 @@ 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 open DefAttributes in
+  let atts = parse 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;
@@ -983,7 +1006,8 @@ let vernac_identity_coercion ~atts id qids qidt =
 (* Type classes *)
 
 let vernac_instance ~atts abst sup inst props pri =
-  let atts = attributes_of_flags atts in
+  let open DefAttributes in
+  let atts = parse 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