Doc for sort poly

I have no idea why sorts.rst goes on about template poly in

~~~quote
the base universe (the expression
:math:`0`) which corresponds, in the arity of template polymorphic inductive
types (see Section
:ref:`well-formed-inductive-definitions`),
to the predicative sort :math:`\Set`
~~~

so I simplified to just "the base universe Set".

The `type@{Prop}` error escaped the box in my local refman-html test
so I inserted a break.

doc/changelog/01-kernel/17836-sort-poly.rst

@@ -0,0 +1,5 @@
+- **Added:**
+  :ref:`sort-polymorphism` makes it possible to share common constructs
+  over `Type` `Prop` and `SProp`
+  (`#17836 <https://github.com/coq/coq/pull/17836>`_,
+  by Gaëtan Gilbert).

doc/sphinx/addendum/universe-polymorphism.rst

@@ -740,6 +740,69 @@ underscore or by omitting the annotation to a polymorphic definition.
 
       About baz.
 
+.. _sort-polymorphism:
+
+Sort polymorphism
+-----------------
+
+Quantifying over universes does not allow instantiation with `Prop` or `SProp`. For instance
+
+.. coqtop:: in reset
+
+   Polymorphic Definition type@{u} := Type@{u}.
+
+.. coqtop:: all
+
+   Fail Check type@{Prop}.
+
+To be able to instantiate a sort with `Prop` or `SProp`, we must
+quantify over :gdef:`sort qualities`. Definitions which quantify over
+sort qualities are called :gdef:`sort polymorphic`.
+
+All sort quality variables must be explicitly bound.
+
+.. coqtop:: all
+
+   Polymorphic Definition sort@{s | u |} := Type@{s|u}.
+
+To help the parser, both `|` in the :n:`@univ_decl` are required.
+
+Sort quality variables of a sort polymorphic definition may be
+instantiated by the concrete values `SProp`, `Prop` and `Type` or by a
+bound variable.
+
+Instantiating `s` in `Type@{s|u}` with the impredicative `Prop` or
+`SProp` produces `Prop` or `SProp` respectively regardless of the
+instantiation fof `u`.
+
+.. coqtop:: all
+
+   Eval cbv in sort@{Prop|Set}.
+   Eval cbv in sort@{Type|Set}.
+
+When no explicit instantiation is provided or `_` is used, a temporary
+variable is generated. Temporary sort variables are instantiated with
+`Type` if not unified with another quality when universe minimization
+runs (typically at the end of a definition).
+
+:cmd:`Check` and :cmd:`Eval` run minimization so we cannot use them to
+witness these temporary variables.
+
+.. coqtop:: in
+
+   Goal True.
+   Set Printing Universes.
+
+.. coqtop:: all abort
+
+   let c := constr:(sort) in idtac c.
+
+.. note::
+
+   We recommend you do not name explicitly quantified sort variables
+   `α` followed by a number as printing will not distinguish between
+   your bound variables and temporary variables.
+
 .. _universe-polymorphism-in-sections:
 
 Universe polymorphism and sections

doc/sphinx/language/core/sorts.rst

@@ -71,31 +71,30 @@ Formally, we call :math:`\Sort` the set of sorts which is defined by:
 Their properties, such as :math:`\Prop:\Type(1)`, :math:`\Set:\Type(1)`, and
 :math:`\Type(i):\Type(i+1)`, are described in :ref:`subtyping-rules`.
 
-The user does not have to mention explicitly the index :math:`i` when
-referring to the universe :math:`\Type(i)`. One only writes `Type`. The system
-itself generates for each instance of `Type` a new index for the
+**Algebraic universes** In practice, the Type hierarchy is
+implemented using algebraic universes,
+which appear in the syntax :n:`Type@{@universe}`.
+An :gdef:`algebraic universe` :math:`u` is either a variable,
+a successor of an algebraic universe (an expression :math:`u+1`),
+an upper bound of algebraic universes (an expression :math:`\max(u_1 ,...,u_n )`),
+or the base universe :math:`\Set`.
+
+A graph of constraints between the universe variables is maintained
+globally. To ensure the existence of a mapping of the universes to the
+positive integers, the graph of constraints must remain acyclic.
+Typing expressions that violate the acyclicity of the graph of
+constraints results in a :exn:`Universe inconsistency` error.
+
+The user does not have to mention explicitly the universe :math:`u` when
+referring to the universe `Type@{u}`. One only writes `Type`. The system
+itself generates for each instance of `Type` a new variable for the
 universe and checks that the constraints between these indexes can be
 solved. From the user point of view we consequently have :math:`\Type:\Type`. We
 shall make precise in the typing rules the constraints between the
 indices.
 
-
-.. _Implementation-issues:
-
-**Implementation issues** In practice, the Type hierarchy is
-implemented using algebraic universes.
-An :gdef:`algebraic universe` :math:`u` is either a variable (a qualified
-identifier with a number) or a successor of an algebraic universe (an
-expression :math:`u+1`), or an upper bound of algebraic universes (an
-expression :math:`\max(u_1 ,...,u_n )`), or the base universe (the expression
-:math:`0`) which corresponds, in the arity of template polymorphic inductive
-types (see Section
-:ref:`well-formed-inductive-definitions`),
-to the predicative sort :math:`\Set`. A graph of
-constraints between the universe variables is maintained globally. To
-ensure the existence of a mapping of the universes to the positive
-integers, the graph of constraints must remain acyclic. Typing
-expressions that violate the acyclicity of the graph of constraints
-results in a :exn:`Universe inconsistency` error.
+The syntax :n:`Type@{@qualid | @universe}` is used with
+:ref:`polymorphicuniverses` when quantifying over all sorts including
+:math:`\Prop` and :math:`\SProp`.
 
 .. seealso:: :ref:`printing-universes`, :ref:`explicit-universes`.

pretyping/pretyping.ml

@@ -157,8 +157,8 @@ let glob_level ?loc evd : glob_level -> _ = function
     match level_name evd s with
     | None ->
       user_err ?loc
-        (str "Universe instances cannot contain non-Set small levels, polymorphic" ++
-        str " universe instances must be greater or equal to Set.");
+        (str "Universe instances cannot contain non-Set small levels," ++ spc() ++
+         str "polymorphic universe instances must be greater or equal to Set.");
     | Some r -> r
 
 let glob_qvar ?loc evd : glob_qvar -> _ = function