diff options
| -rw-r--r-- | vernac/attributes.ml | 5 | ||||
| -rw-r--r-- | vernac/attributes.mli | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 9 |
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 |