5 files changed, 53 insertions, 25 deletions
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index cfaa681d20..a6dc15da55 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -37,6 +37,8 @@ In addition to these user-defined classes, we have two built-in classes:
   * ``Funclass``, the class of functions; its objects are all the terms with a functional
     type, i.e. of form :g:`forall x:A,B`.
 
+Formally, the syntax of classes is defined as:
+
    .. insertprodn class class
 
    .. prodn::
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index 082ea4691b..e1b1ee8e8d 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -1,4 +1,4 @@
-.. _omega:
+.. _omega_chapter:
 
 Omega: a solver for quantifier-free problems in Presburger Arithmetic
 =====================================================================
@@ -28,6 +28,7 @@ Description of ``omega``
 ------------------------
 
 .. tacn:: omega
+   :name: omega
 
    .. deprecated:: 8.12
 
diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
index 9acdd18b89..b19239ed22 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -7,27 +7,26 @@ SProp (proof irrelevant propositions)
 
    The status of strict propositions is experimental.
 
+   In particular, conversion checking through bytecode or native code
+   compilation currently does not understand proof irrelevance.
+
 This section describes the extension of |Coq| with definitionally
 proof irrelevant propositions (types in the sort :math:`\SProp`, also
 known as strict propositions) as described in
 :cite:`Gilbert:POPL2019`.
 
-Using :math:`\SProp` may be prevented by passing ``-disallow-sprop``
-to the |Coq| program or using :flag:`Allow StrictProp`.
+Use of |SProp| may be disabled by passing ``-disallow-sprop`` to the
+|Coq| program or by turning the :flag:`Allow StrictProp` flag off.
 
 .. flag:: Allow StrictProp
    :name: Allow StrictProp
 
-   Allows using :math:`\SProp` when set and forbids it when unset. The
-   initial value depends on whether you used the command line
-   ``-disallow-sprop`` and ``-allow-sprop``.
-
-.. exn:: SProp not allowed, you need to Set Allow StrictProp or to use the -allow-sprop command-line-flag.
-   :undocumented:
-
-.. coqtop:: none
+   Enables or disables the use of |SProp|.  It is enabled by default.
+   The command-line flag ``-disallow-sprop`` disables |SProp| at
+   startup.
 
-   Set Allow StrictProp.
+   .. exn:: SProp is disallowed because the "Allow StrictProp" flag is off.
+      :undocumented:
 
 Some of the definitions described in this document are available
 through ``Coq.Logic.StrictProp``, which see.
@@ -38,29 +37,35 @@ Basic constructs
 The purpose of :math:`\SProp` is to provide types where all elements
 are convertible:
 
-.. coqdoc::
+.. coqtop:: all
 
-   Definition irrelevance (A:SProp) (P:A -> Prop) (x:A) (v:P x) (y:A) : P y := v.
+   Theorem irrelevance (A : SProp) (P : A -> Prop) : forall x : A, P x -> forall y : A, P y.
+   Proof.
+   intros * Hx *.
+   exact Hx.
+   Qed.
 
 Since we have definitional :ref:`eta-expansion` for
 functions, the property of being a type of definitionally irrelevant
 values is impredicative, and so is :math:`\SProp`:
 
-.. coqdoc::
+.. coqtop:: all
 
    Check fun (A:Type) (B:A -> SProp) => (forall x:A, B x) : SProp.
 
-.. warning::
-
-   Conversion checking through bytecode or native code compilation
-   currently does not understand proof irrelevance.
-
 In order to keep conversion tractable, cumulativity for :math:`\SProp`
-is forbidden:
+is forbidden, unless the :flag:`Cumulative StrictProp` flag is turned
+on:
 
 .. coqtop:: all
 
    Fail Check (fun (A:SProp) => A : Type).
+   Set Cumulative StrictProp.
+   Check (fun (A:SProp) => A : Type).
+
+.. coqtop:: none
+
+   Unset Cumulative StrictProp.
 
 We can explicitly lift strict propositions into the relevant world by
 using a wrapping inductive type. The inductive stops definitional
@@ -240,3 +245,10 @@ so correctly converts ``x`` and ``y``.
   the kernel when it is passed a term with incorrect relevance marks.
   To avoid conversion issues as in ``late_mark`` you may wish to use
   it to find when your tactics are producing incorrect marks.
+
+.. flag:: Cumulative StrictProp
+   :name: Cumulative StrictProp
+
+   Set this flag (it is off by default) to make the kernel accept
+   cumulativity between |SProp| and other universes. This makes
+   typechecking incomplete.
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index bd4c276571..903aa266e2 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -241,7 +241,7 @@ binders. For example:
 
    Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := andb (le x y) (neqb x y).
 
-The ``!`` modifier switches the way a binder is parsed back to the regular
+The ``!`` modifier switches the way a binder is parsed back to the usual
 interpretation of Coq. In particular, it uses the implicit arguments
 mechanism if available, as shown in the example.
 
@@ -323,7 +323,7 @@ Summary of the commands
 
    .. cmdv:: Existing Class @ident
 
-      This variant declares a class a posteriori from a constant or
+      This variant declares a class from a previously declared constant or
       inductive definition. No methods or instances are defined.
 
       .. warn:: @ident is already declared as a typeclass
@@ -394,7 +394,7 @@ few other commands related to typeclasses.
    :name: typeclasses eauto
 
    This proof search tactic implements the resolution engine that is run
-   implicitly during type-checking. This tactic uses a different resolution
+   implicitly during type checking. This tactic uses a different resolution
    engine than :tacn:`eauto` and :tacn:`auto`. The main differences are the
    following:
 
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index a08495badd..2958d866ac 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -227,7 +227,7 @@ constraints by prefixing the level names with symbols.
 Because inductive subtypings are only produced by comparing inductives
 to themselves with universes changed, they amount to variance
 information: each universe is either invariant, covariant or
-irrelevant (there are no contravariant subtypings in Coq),
+irrelevant (there are no contravariant subtypings in |Coq|),
 respectively represented by the symbols `=`, `+` and `*`.
 
 Here we see that :g:`list` binds an irrelevant universe, so any two
@@ -426,6 +426,19 @@ mode, introduced universe names can be referred to in terms. Note that
 local universe names shadow global universe names. During a proof, one
 can use :cmd:`Show Universes` to display the current context of universes.
 
+It is possible to provide only some universe levels and let |Coq| infer the others
+by adding a :g:`+` in the list of bound universe levels:
+
+.. coqtop:: all
+
+   Fail Definition foobar@{u} : Type@{u} := Type.
+   Definition foobar@{u +} : Type@{u} := Type.
+   Set Printing Universes.
+   Print foobar.
+
+This can be used to find which universes need to be explicitly bound in a given
+definition.
+
 Definitions can also be instantiated explicitly, giving their full
 instance: