Move template out of Defattributes record

3 files changed, 7 insertions, 9 deletions

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 9ab8f7c8fd..4f238f38e6 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -173,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 >>
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index a3e85172e8..6a32960a9d 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -49,7 +49,7 @@ 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
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d932b4cb16..39be6af179 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -57,17 +57,16 @@ module DefAttributes = struct
   type t = {
     locality : bool option;
     polymorphic : bool;
-    template : bool option;
     program : bool;
     deprecated : deprecation option;
   }
 
   let parse f =
     let open Attributes in
-    let ((locality, deprecated), (polymorphic, template)), program =
-      parse Notations.(locality ++ deprecation ++ universe_poly_template ++ program) f
+    let ((locality, deprecated), polymorphic), program =
+      parse Notations.(locality ++ deprecation ++ polymorphic ++ program) f
     in
-    { polymorphic; program; locality; template; deprecated }
+    { polymorphic; program; locality; deprecated }
 end
 
 (*******************)
@@ -657,6 +656,7 @@ let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) =
     neither. *)
 let vernac_inductive ~atts cum lo finite indl =
   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
@@ -682,7 +682,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