5 files changed, 49 insertions, 9 deletions
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst
index 45b3f6f161..15f42591ce 100644
--- a/doc/sphinx/addendum/extended-pattern-matching.rst
+++ b/doc/sphinx/addendum/extended-pattern-matching.rst
@@ -192,7 +192,7 @@ Disjunctive patterns
 --------------------
 
 Multiple patterns that share the same right-hand-side can be
-factorized using the notation :n:`{+| @patterns_comma}`. For
+factorized using the notation :n:`{+| {+, @pattern } }`. For
 instance, :g:`max` can be rewritten as follows:
 
 .. coqtop:: in reset
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst
index 7136cc28d1..d909f98956 100644
--- a/doc/sphinx/addendum/extraction.rst
+++ b/doc/sphinx/addendum/extraction.rst
@@ -313,14 +313,21 @@ The system also provides a mechanism to specify ML terms for inductive
 types and constructors. For instance, the user may want to use the ML
 native boolean type instead of the |Coq| one. The syntax is the following:
 
-.. cmd:: Extract Inductive @qualid => @string [ {+ @string } ]
+.. cmd:: Extract Inductive @qualid => @string__1 [ {+ @string } ]
 
    Give an ML extraction for the given inductive type. You must specify
-   extractions for the type itself (first :token:`string`) and all its
-   constructors (all the :token:`string` between square brackets). In this form,
+   extractions for the type itself (:n:`@string__1`) and all its
+   constructors (all the :n:`@string` between square brackets). In this form,
    the ML extraction must be an ML inductive datatype, and the native
    pattern matching of the language will be used.
 
+   When :n:`@string__1` matches the name of the type of characters or strings
+   (``char`` and ``string`` for OCaml, ``Prelude.Char`` and ``Prelude.String``
+   for Haskell), extraction of literals is handled in a specialized way, so as
+   to generate literals in the target language. This feature requires the type
+   designated by :n:`@qualid` to be registered as the standard char or string type,
+   using the :cmd:`Register` command.
+
 .. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string
 
    Same as before, with a final extra :token:`string` that indicates how to
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index 650a444a16..daca43e65e 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -5,6 +5,27 @@ Omega: a solver for quantifier-free problems in Presburger Arithmetic
 
 :Author: Pierre Crégut
 
+.. 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`.
+
+   Note that replacing :tacn:`omega` with :tacn:`lia` can break
+   non-robust proof scripts which rely on incompleteness bugs of
+   :tacn:`omega` (e.g. using the pattern :g:`; try omega`).
+
 Description of ``omega``
 ------------------------
 
diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst
index 35729d852d..7a50748c51 100644
--- a/doc/sphinx/addendum/parallel-proof-processing.rst
+++ b/doc/sphinx/addendum/parallel-proof-processing.rst
@@ -154,6 +154,18 @@ to a worker process. The threshold can be configured with
 Batch mode
 ---------------
 
+   .. warning::
+
+      The ``-vio`` flag is subsumed, for most practical usage, by the
+      the more recent ``-vos`` flag. See :ref:`compiled-interfaces`.
+
+   .. warning::
+
+      When working with ``.vio`` files, do not use the ``-vos`` option at
+      the same time, otherwise stale files might get loaded when executing
+      a ``Require``. Indeed, the loading of a nonempty ``.vos`` file is
+      assigned higher priority than the loading of a ``.vio`` file.
+
 When |Coq| is used as a batch compiler by running ``coqc``, it produces
 a ``.vo`` file for each ``.v`` file. A ``.vo`` file contains, among other
 things, theorem statements and proofs. Hence to produce a .vo |Coq|
@@ -161,10 +173,10 @@ need to process all the proofs of the ``.v`` file.
 
 The asynchronous processing of proofs can decouple the generation of a
 compiled file (like the ``.vo`` one) that can be loaded by ``Require`` from the
-generation and checking of the proof objects. The ``-quick`` flag can be
+generation and checking of the proof objects. The ``-vio`` flag can be
 passed to ``coqc`` to produce, quickly, ``.vio`` files.
 Alternatively, when using a Makefile produced by ``coq_makefile``,
-the ``quick`` target can be used to compile all files using the ``-quick`` flag.
+the ``vio`` target can be used to compile all files using the ``-vio`` flag.
 
 A ``.vio`` file can be loaded using ``Require`` exactly as a ``.vo`` file but
 proofs will not be available (the Print command produces an error).
@@ -173,7 +185,7 @@ inconsistencies might go unnoticed. A ``.vio`` file does not contain proof
 objects, but proof tasks, i.e. what a worker process can transform
 into a proof object.
 
-Compiling a set of files with the ``-quick`` flag allows one to work,
+Compiling a set of files with the ``-vio`` flag allows one to work,
 interactively, on any file without waiting for all the proofs to be
 checked.
 
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 7adb25cbd6..f9cc25959c 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -529,8 +529,8 @@ sections, except in the following ways:
        Polymorphic Universe i.
        Fail Constraint i = i.
 
-  This includes constraints implictly declared by commands such as
-  :cmd:`Variable`, which may as a such need to be used with universe
+  This includes constraints implicitly declared by commands such as
+  :cmd:`Variable`, which may need to be used with universe
   polymorphism activated (locally by attribute or globally by option):
 
   .. coqtop:: all