Remove unqualified universe attributes.

They were already deprecated in two major releases.

3 files changed, 6 insertions, 27 deletions

diff --git a/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst b/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst
new file mode 100644
index 0000000000..1f8dcd3992
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/11663-remove-polymorphic-unqualified.rst
@@ -0,0 +1,5 @@
+- **Removed:**
+  Unqualified ``polymorphic``, ``monomorphic``, ``template``,
+  ``notemplate`` attributes (they were deprecated since Coq 8.10).
+  Use them as sub-attributes of the ``universes`` attribute (`#11663
+  <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann).
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 194308b77f..7213ba4829 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -163,23 +163,7 @@ let program =
 
 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 =
@@ -198,16 +182,10 @@ let polymorphic_base =
   | Some b -> return b
   | None -> return (is_universe_polymorphism())
 
-let polymorphic_nowarn =
-  universe_transform ~warn_unqualified:false >>
-  qualify_attribute ukey polymorphic_base
-
 let template =
-  universe_transform ~warn_unqualified:true >>
   qualify_attribute ukey (bool_attribute ~name:"Template" ~on:"template" ~off:"notemplate")
 
 let polymorphic =
-  universe_transform ~warn_unqualified:true >>
   qualify_attribute ukey polymorphic_base
 
 let deprecation_parser : Deprecation.t key_parser = fun orig args ->
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 0074db66d3..7ecb7e4fb0 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -114,10 +114,6 @@ val make_attribute : (vernac_flags -> vernac_flags * 'a) -> 'a attribute
 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)]. *)
+(** For internal use. *)
 val universe_polymorphism_option_name : string list
 val is_universe_polymorphism : unit -> bool