6 files changed, 47 insertions, 22 deletions
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 1f33775a01..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::
@@ -257,7 +259,7 @@ Activating the Printing of Coercions
    :name: Printing Coercion
 
    Specifies a set of qualids for which coercions are always displayed.  Use the
-   :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids.
+   :cmd:`Add` and :cmd:`Remove` commands to update the set of qualids.
 
 .. _coercions-classes-as-records:
 
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index f706633da9..77bf58aac6 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -1,4 +1,4 @@
-.. _ micromega:
+.. _micromega:
 
 Micromega: tactics for solving arithmetic goals over ordered rings
 ==================================================================
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index daca43e65e..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
 =====================================================================
@@ -7,20 +7,18 @@ Omega: a solver for quantifier-free problems in Presburger Arithmetic
 
 .. warning::
 
-   The :tacn:`omega` tactic is about to be deprecated in favor of the
-   :tacn:`lia` tactic.  The goal is to consolidate the arithmetic
-   solving capabilities of Coq into a single engine; moreover,
-   :tacn:`lia` is in general more powerful than :tacn:`omega` (it is a
-   complete Presburger arithmetic solver while :tacn:`omega` was known
-   to be incomplete).
-
-   Work is in progress to make sure that there are no regressions
-   (including no performance regression) when switching from
-   :tacn:`omega` to :tacn:`lia` in existing projects.  However, we
-   already recommend using :tacn:`lia` in new or refactored proof
-   scripts.  We also ask that you report (in our `bug tracker
-   <https://github.com/coq/coq/issues>`_) any issue you encounter,
-   especially if the issue was not present in :tacn:`omega`.
+   The :tacn:`omega` tactic is deprecated in favor of the :tacn:`lia`
+   tactic.  The goal is to consolidate the arithmetic solving
+   capabilities of Coq into a single engine; moreover, :tacn:`lia` is
+   in general more powerful than :tacn:`omega` (it is a complete
+   Presburger arithmetic solver while :tacn:`omega` was known to be
+   incomplete).
+
+   It is recommended to switch from :tacn:`omega` to :tacn:`lia` in existing
+   projects.  We also ask that you report (in our `bug tracker
+   <https://github.com/coq/coq/issues>`_) any issue you encounter, especially
+   if the issue was not present in :tacn:`omega`.  If no new issues are
+   reported, :tacn:`omega` will be removed soon.
 
    Note that replacing :tacn:`omega` with :tacn:`lia` can break
    non-robust proof scripts which rely on incompleteness bugs of
@@ -30,6 +28,11 @@ Description of ``omega``
 ------------------------
 
 .. tacn:: omega
+   :name: omega
+
+   .. deprecated:: 8.12
+
+      Use :tacn:`lia` instead.
 
    :tacn:`omega` is a tactic for solving goals in Presburger arithmetic,
    i.e. for proving formulas made of equations and inequalities over the
@@ -118,7 +121,7 @@ loaded by
 
 .. example::
 
-  .. coqtop:: all
+  .. coqtop:: all warn
 
      Require Import Omega.
 
diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
index 9acdd18b89..b2d3687780 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -240,3 +240,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: