Doc for variance syntax

3 files changed, 30 insertions, 2 deletions

diff --git a/doc/changelog/02-specification-language/12653-cumul-syntax.rst b/doc/changelog/02-specification-language/12653-cumul-syntax.rst
new file mode 100644
index 0000000000..b6c87ed4b6
--- /dev/null
+++ b/doc/changelog/02-specification-language/12653-cumul-syntax.rst
@@ -0,0 +1,4 @@
+- **Added:** Syntax for specifying the variance of cumulative
+  polymorphic inductives (:ref:`cumulative`) instead of letting it be
+  inferred (`#12653 <https://github.com/coq/coq/pull/12653>`_, by
+  Gaëtan Gilbert).
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 1fb337b30a..064107d088 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -246,6 +246,7 @@ The following is an example of a record with non-trivial subtyping relation:
 .. coqtop:: all
 
    Polymorphic Cumulative Record packType := {pk : Type}.
+   About packType.
 
 :g:`packType` binds a covariant universe, i.e.
 
@@ -254,6 +255,27 @@ The following is an example of a record with non-trivial subtyping relation:
    E[Γ] ⊢ \mathsf{packType}@\{i\} =_{βδιζη}
    \mathsf{packType}@\{j\}~\mbox{ whenever }~i ≤ j
 
+Specifying cumulativity
+~~~~~~~~~~~~~~~~~~~~~~~
+
+The variance of the universe parameters for a cumulative inductive may be specified by the user.
+
+For the following type, universe ``a`` has its variance automatically
+inferred (it is irrelevant), ``b`` is required to be irrelevant,
+``c`` is covariant and ``d`` is invariant. With these annotations
+``c`` and ``d`` have less general variances than would be inferred.
+
+.. coqtop:: all
+
+   Polymorphic Cumulative Inductive Dummy@{a *b +c =d} : Prop := dummy.
+   About Dummy.
+
+Insufficiently restrictive variance annotations lead to errors:
+
+.. coqtop:: all
+
+   Fail Polymorphic Cumulative Record bad@{*a} := {p : Type@{a}}.
+
 An example of a proof using cumulativity
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -280,7 +302,7 @@ An example of a proof using cumulativity
    End down.
 
 Cumulativity Weak Constraints
------------------------------
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. flag:: Cumulativity Weak Constraints
 
@@ -383,6 +405,7 @@ Explicit Universes
    | _
    | @qualid
    univ_decl ::= @%{ {* @ident } {? + } {? %| {*, @univ_constraint } {? + } } %}
+   cumul_univ_decl ::= @%{ {* {? {| = | + | * } } @ident } {? + } {? %| {*, @univ_constraint } {? + } } %}
    univ_constraint ::= @universe_name {| < | = | <= } @universe_name
 
 The syntax has been extended to allow users to explicitly bind names
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index d3bd787587..7bb03d7d85 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -11,10 +11,11 @@ Inductive types
    .. insertprodn inductive_definition constructor
 
    .. prodn::
-      inductive_definition ::= {? > } @ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations }
+      inductive_definition ::= {? > } @cumul_ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations }
       constructors_or_record ::= {? %| } {+| @constructor }
       | {? @ident } %{ {*; @record_field } {? ; } %}
       constructor ::= @ident {* @binder } {? @of_type }
+      cumul_ident_decl ::=  @ident {? @cumul_univ_decl }
 
    This command defines one or more
    inductive types and its constructors.  Coq generates destructors