14 files changed, 117 insertions, 93 deletions
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 3b9760f586..c0a57763b9 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -27,6 +27,13 @@ rationals ``Require Import Lqa`` and reals ``Require Import Lra``.
   generating a *proof cache* which makes it possible to rerun scripts
   even without `csdp`.
 
+.. flag:: Simplex
+
+   This option (set by default) instructs the decision procedures to
+   use the Simplex method for solving linear goals. If it is not set,
+   the decision procedures are using Fourier elimination.
+
+
 The tactics solve propositional formulas parameterized by atomic
 arithmetic expressions interpreted over a domain :math:`D` ∈ {ℤ, ℚ, ℝ}.
 The syntax of the formulas is the following:
@@ -96,8 +103,7 @@ and checked to be :math:`-1`.
 .. tacn:: lra
    :name: lra
 
-   This tactic is searching for *linear* refutations using Fourier
-   elimination [#]_. As a result, this tactic explores a subset of the *Cone*
+   This tactic is searching for *linear* refutations. As a result, this tactic explores a subset of the *Cone*
    defined as
 
    :math:`\mathit{LinCone}(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p~\right|~\alpha_p \mbox{ are positive constants} \right\}`
@@ -134,7 +140,7 @@ principle [#]_. However, this is not the case over :math:`\mathbb{Z}`. Actually,
 *positivstellensatz* refutations are not even sufficient to decide
 linear *integer* arithmetic. The canonical example is :math:`2 * x = 1 -> \mathtt{False}`
 which is a theorem of :math:`\mathbb{Z}` but not a theorem of :math:`{\mathbb{R}}`. To remedy this
-weakness, the `lia` tactic is using recursively a combination of:
+weakness, the :tacn:`lia` tactic is using recursively a combination of:
 
 + linear *positivstellensatz* refutations;
 + cutting plane proofs;
@@ -188,10 +194,10 @@ a proof.
 .. tacn:: nra
    :name: nra
 
-This tactic is an *experimental* proof procedure for non-linear
-arithmetic. The tactic performs a limited amount of non-linear
-reasoning before running the linear prover of `lra`. This pre-processing
-does the following:
+   This tactic is an *experimental* proof procedure for non-linear
+   arithmetic. The tactic performs a limited amount of non-linear
+   reasoning before running the linear prover of :tacn:`lra`. This pre-processing
+   does the following:
 
 
 + If the context contains an arithmetic expression of the form
@@ -200,7 +206,7 @@ does the following:
 + For all pairs of hypotheses :math:`e_1 \ge 0`, :math:`e_2 \ge 0`, the context is
   enriched with :math:`e_1 \times e_2 \ge 0`.
 
-After this pre-processing, the linear prover of `lra` searches for a
+After this pre-processing, the linear prover of :tacn:`lra` searches for a
 proof by abstracting monomials by variables.
 
 `nia`: a proof procedure for non-linear integer arithmetic
@@ -209,9 +215,9 @@ proof by abstracting monomials by variables.
 .. tacn:: nia
    :name: nia
 
-This tactic is a proof procedure for non-linear integer arithmetic.
-It performs a pre-processing similar to `nra`. The obtained goal is
-solved using the linear integer prover `lia`.
+   This tactic is a proof procedure for non-linear integer arithmetic.
+   It performs a pre-processing similar to :tacn:`nra`. The obtained goal is
+   solved using the linear integer prover :tacn:`lia`.
 
 `psatz`: a proof procedure for non-linear arithmetic
 ----------------------------------------------------
@@ -219,22 +225,22 @@ solved using the linear integer prover `lia`.
 .. tacn:: psatz
    :name: psatz
 
-This tactic explores the :math:`\mathit{Cone}` by increasing degrees – hence the
-depth parameter :math:`n`. In theory, such a proof search is complete – if the
-goal is provable the search eventually stops. Unfortunately, the
-external oracle is using numeric (approximate) optimization techniques
-that might miss a refutation.
+   This tactic explores the *Cone* by increasing degrees – hence the
+   depth parameter *n*. In theory, such a proof search is complete – if the
+   goal is provable the search eventually stops. Unfortunately, the
+   external oracle is using numeric (approximate) optimization techniques
+   that might miss a refutation.
 
-To illustrate the working of the tactic, consider we wish to prove the
-following Coq goal:
+   To illustrate the working of the tactic, consider we wish to prove the
+   following Coq goal:
 
 .. coqtop:: all
 
-  Require Import ZArith Psatz.
-  Open Scope Z_scope.
-  Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
-  intro x.
-  psatz Z 2.
+   Require Import ZArith Psatz.
+   Open Scope Z_scope.
+   Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
+   intro x.
+   psatz Z 2.
 
 As shown, such a goal is solved by ``intro x. psatz Z 2.``. The oracle returns the
 cone expression :math:`2 \times (x-1) + (\mathbf{x-1}) \times (\mathbf{x−1}) + -x^2`
@@ -246,7 +252,6 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
   the `zify` tactic.
 .. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp
 .. [#] Variants deal with equalities and strict inequalities.
-.. [#] More efficient linear programming techniques could equally be employed.
 .. [#] In practice, the oracle might fail to produce such a refutation.
 
 .. comment in original TeX:
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 71f01cbb17..d98b8641e9 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -193,8 +193,9 @@ html_theme = 'sphinx_rtd_theme'
 # Theme options are theme-specific and customize the look and feel of a theme
 # further.  For a list of options available for each theme, see the
 # documentation.
-#html_theme_options = {}
-
+html_theme_options = {
+    'collapse_navigation': False
+}
 html_context = {
     'display_github': True,
     'github_user': 'coq',
diff --git a/doc/sphinx/credits.html.rst b/doc/sphinx/credits.html.rst
deleted file mode 100644
index 0b2b1c6ad1..0000000000
--- a/doc/sphinx/credits.html.rst
+++ /dev/null
@@ -1,7 +0,0 @@
-.. _credits:
-
--------
-Credits
--------
-
-.. include:: credits-contents.rst
diff --git a/doc/sphinx/credits.latex.rst b/doc/sphinx/credits.latex.rst
deleted file mode 100644
index 39101f9d52..0000000000
--- a/doc/sphinx/credits.latex.rst
+++ /dev/null
@@ -1,3 +0,0 @@
-.. _credits:
-
-.. include:: credits-contents.rst
diff --git a/doc/sphinx/credits-contents.rst b/doc/sphinx/credits.rst
index d1df0657aa..ffdc4f3ec6 100644
--- a/doc/sphinx/credits-contents.rst
+++ b/doc/sphinx/credits.rst
@@ -1,3 +1,7 @@
+-------
+Credits
+-------
+
 Coq is a proof assistant for higher-order logic, allowing the
 development of computer programs consistent with their formal
 specification. It is the result of about ten years of research of the
@@ -186,7 +190,7 @@ definitions of “inversion predicates”.
 |
 
 Credits: addendum for version 6.1
-=================================
+---------------------------------
 
 The present version 6.1 of |Coq| is based on the V5.10 architecture. It
 was ported to the new language Objective Caml by Bruno Barras. The
@@ -223,7 +227,7 @@ Barras.
 |
 
 Credits: addendum for version 6.2
-=================================
+---------------------------------
 
 In version 6.2 of |Coq|, the parsing is done using camlp4, a preprocessor
 and pretty-printer for CAML designed by Daniel de Rauglaudre at INRIA.
@@ -268,7 +272,7 @@ Loiseleur.
 |
 
 Credits: addendum for version 6.3
-=================================
+---------------------------------
 
 The main changes in version V6.3 were the introduction of a few new
 tactics and the extension of the guard condition for fixpoint
@@ -301,7 +305,7 @@ Monin from CNET Lannion.
 |
 
 Credits: versions 7
-===================
+-------------------
 
 The version V7 is a new implementation started in September 1999 by
 Jean-Christophe Filliâtre. This is a major revision with respect to the
@@ -390,7 +394,7 @@ J.-F. Monin from France Telecom R & D.
 |
 
 Credits: version 8.0
-====================
+--------------------
 
 Coq version 8 is a major revision of the |Coq| proof assistant. First, the
 underlying logic is slightly different. The so-called *impredicativity*
@@ -492,7 +496,7 @@ under the responsibility of Christine Paulin.
 |
 
 Credits: version 8.1
-====================
+--------------------
 
 Coq version 8.1 adds various new functionalities.
 
@@ -571,7 +575,7 @@ and Yale University.
 |
 
 Credits: version 8.2
-====================
+--------------------
 
 Coq version 8.2 adds new features, new libraries and improves on many
 various aspects.
@@ -665,7 +669,7 @@ the Coq-Club mailing list.
 |
 
 Credits: version 8.3
-====================
+--------------------
 
 Coq version 8.3 is before all a transition version with refinements or
 extensions of the existing features and libraries and a new tactic nsatz
@@ -739,7 +743,7 @@ Pierce for the excellent teaching materials they provided.
 |
 
 Credits: version 8.4
-====================
+--------------------
 
 Coq version 8.4 contains the result of three long-term projects: a new
 modular library of arithmetic by Pierre Letouzey, a new proof engine by
@@ -895,7 +899,7 @@ Eelis van der Weegen.
 |
 
 Credits: version 8.5
-====================
+--------------------
 
 Coq version 8.5 contains the result of five specific long-term projects:
 
@@ -1049,7 +1053,7 @@ Tankink. Maxime Dénès coordinated the release process.
 |
 
 Credits: version 8.6
-====================
+--------------------
 
 Coq version 8.6 contains the result of refinements, stabilization of
 8.5’s features and cleanups of the internals of the system. Over the
@@ -1189,7 +1193,8 @@ Dénès to put together a |Coq| consortium.
 |
 
 Credits: version 8.7
-====================
+--------------------
+
 |Coq| version 8.7 contains the result of refinements, stabilization of features
 and cleanups of the internals of the system along with a few new features. The
 main user visible changes are:
@@ -1294,8 +1299,7 @@ system, is now upcoming and will rely on Inria’s newly created Foundation.
 |
 
 Credits: version 8.8
-====================
-
+--------------------
 
 |Coq| version 8.8 contains the result of refinements and stabilization of
 features and deprecations, cleanups of the internals of the system along
diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst
index cf12b57414..a652b9e1ca 100644
--- a/doc/sphinx/index.html.rst
+++ b/doc/sphinx/index.html.rst
@@ -1,13 +1,11 @@
-.. _introduction:
-
 ==========================
-Introduction
+Introduction and Contents
 ==========================
 
 .. include:: introduction.rst
 
-Table of contents
------------------
+Contents
+--------
 
 .. toctree::
    :caption: Indexes
@@ -82,9 +80,6 @@ Table of contents
 
    zebibliography
 
-License
--------
-
 .. include:: license.rst
 
 .. [#PG] Proof-General is available at https://proofgeneral.github.io/.
diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst
index af757f8746..9e9eb330fe 100644
--- a/doc/sphinx/index.latex.rst
+++ b/doc/sphinx/index.latex.rst
@@ -2,26 +2,22 @@
  The Coq Reference Manual
 ==========================
 
+------------
 Introduction
 ------------
 
 .. include:: introduction.rst
 
+.. include:: license.rst
+
 .. [#PG] Proof-General is available at https://proofgeneral.github.io/.
    Optionally, you can enhance it with the minor mode
    Company-Coq :cite:`Pit16`
    (see https://github.com/cpitclaudel/company-coq).
 
-Credits
--------
-
 .. include:: credits.rst
 
-License
--------
-
-.. include:: license.rst
-
+------------
 The language
 ------------
 
@@ -33,6 +29,7 @@ The language
    language/cic
    language/module-system
 
+----------------
 The proof engine
 ----------------
 
@@ -45,6 +42,7 @@ The proof engine
    proof-engine/detailed-tactic-examples
    proof-engine/ssreflect-proof-language
 
+---------------
 User extensions
 ---------------
 
@@ -53,6 +51,7 @@ User extensions
    user-extensions/syntax-extensions
    user-extensions/proof-schemes
 
+---------------
 Practical tools
 ---------------
 
@@ -62,6 +61,7 @@ Practical tools
    practical-tools/utilities
    practical-tools/coqide
 
+--------
 Addendum
 --------
 
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
index 5bb7bf542c..bcdf3277ad 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -44,7 +44,7 @@ are processed from a file.
 .. seealso:: :ref:`thecoqcommands`.
 
 How to read this book
-=====================
+---------------------
 
 This is a Reference Manual, so it is not intended for continuous reading.
 We recommend using the various indexes to quickly locate the documentation
@@ -90,7 +90,7 @@ Nonetheless, the manual has some structure that is explained below.
    solvers and tactics. See the table of contents for a complete list.
 
 List of additional documentation
-================================
+--------------------------------
 
 This manual does not contain all the documentation the user may need
 about |Coq|. Various informations can be found in the following documents:
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 593afa8f20..8c82526f0c 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1422,15 +1422,6 @@ using the keyword :cmd:`Qed`.
    #. One can also use :cmd:`Admitted` in place of :cmd:`Qed` to turn the
       current asserted statement into an axiom and exit the proof editing mode.
 
-.. [1]
-   This is similar to the expression “*entry* :math:`\{` sep *entry*
-   :math:`\}`” in standard BNF, or “*entry* :math:`(` sep *entry*
-   :math:`)`\ \*” in the syntax of regular expressions.
-
-.. [2]
-   Except if the inductive type is empty in which case there is no
-   equation that can be used to infer the return type.
-
 .. _gallina-attributes:
 
 Attributes
@@ -1466,12 +1457,14 @@ the following attributes names are recognized:
     This attribute can trigger the following warnings:
 
     .. warn:: Tactic @qualid is deprecated since @string. @string.
+       :undocumented:
 
     .. warn:: Tactic Notation @qualid is deprecated since @string. @string.
+       :undocumented:
 
-Here are a few examples:
+.. example::
 
-.. coqtop:: all reset
+   .. coqtop:: all reset
 
         From Coq Require Program.
         #[program] Definition one : nat := S _.
@@ -1486,3 +1479,12 @@ Here are a few examples:
         Proof.
           now foo.
         Abort.
+
+.. [1]
+   This is similar to the expression “*entry* :math:`\{` sep *entry*
+   :math:`\}`” in standard BNF, or “*entry* :math:`(` sep *entry*
+   :math:`)`\ \*” in the syntax of regular expressions.
+
+.. [2]
+   Except if the inductive type is empty in which case there is no
+   equation that can be used to infer the return type.
diff --git a/doc/sphinx/license.rst b/doc/sphinx/license.rst
index 232b04211c..55c6d988f0 100644
--- a/doc/sphinx/license.rst
+++ b/doc/sphinx/license.rst
@@ -1,3 +1,6 @@
+License
+-------
+
 This material (the Coq Reference Manual) may be distributed only subject to the
 terms and conditions set forth in the Open Publication License, v1.0 or later
 (the latest version is presently available at
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 19995520bb..7c78e1a50f 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -41,15 +41,17 @@ Building a |Coq| project with coq_makefile
 The majority of |Coq| projects are very similar: a collection of ``.v``
 files and eventually some ``.ml`` ones (a |Coq| plugin). The main piece of
 metadata needed in order to build the project are the command line
-options to ``coqc`` (e.g. ``-R``, ``-I``, see also: section
-:ref:`command-line-options`). Collecting the list of files and options is the job
-of the ``_CoqProject`` file.
+options to ``coqc`` (e.g. ``-R``, ``Q``, ``-I``, see :ref:`command
+line options <command-line-options>`). Collecting the list of files
+and options is the job of the ``_CoqProject`` file.
 
 A simple example of a ``_CoqProject`` file follows:
 
 ::
 
     -R theories/ MyCode
+    -arg -w
+    -arg all
     theories/foo.v
     theories/bar.v
     -I src/
@@ -57,6 +59,11 @@ A simple example of a ``_CoqProject`` file follows:
     src/bazaux.ml
     src/qux_plugin.mlpack
 
+where options ``-R``, ``-Q`` and ``-I`` are natively recognized, as well as
+file names. The lines of the form ``-arg foo`` are used in order to tell
+to literally pass an argument ``foo`` to ``coqc``: in the
+example, this allows to pass the two-word option ``-w all`` (see
+:ref:`command line options <command-line-options>`).
 
 Currently, both |CoqIDE| and Proof-General (version ≥ ``4.3pre``)
 understand ``_CoqProject`` files and invoke |Coq| with the desired options.
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 46851050ac..c802f44ac1 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -632,16 +632,15 @@ How to enable diffs
 ```````````````````
 
 .. opt:: Diffs %( "on" %| "off" %| "removed" %)
+   :name: Diffs
 
-  .. This ref doesn't work: :opt:`Set Diffs %( "on" %| "off" %| "removed" %)`
-
-  The “on” option highlights added tokens in green, while the “removed” option
-  additionally reprints items with removed tokens in red.  Unchanged tokens in
-  modified items are shown with pale green or red.  (Colors are user-configurable.)
+   The “on” option highlights added tokens in green, while the “removed” option
+   additionally reprints items with removed tokens in red.  Unchanged tokens in
+   modified items are shown with pale green or red.  (Colors are user-configurable.)
 
 For coqtop, showing diffs can be enabled when starting coqtop with the
-``-diffs on|off|removed`` command-line option or with the ``Set Diffs``
-command within Coq.  You will need to provide the ``-color on|auto`` command-line option when
+``-diffs on|off|removed`` command-line option or by setting the :opt:`Diffs` option
+within Coq.  You will need to provide the ``-color on|auto`` command-line option when
 you start coqtop in either case.
 
 Colors for coqtop can be configured by setting the ``COQ_COLORS`` environment
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index db9f04ba11..26f4ec6242 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -103,7 +103,7 @@ bindings_list`` where ``bindings_list`` may be of two different forms:
 
   .. exn:: Not the right number of missing arguments.
 
-.. _occurencessets:
+.. _occurrencessets:
 
 Occurrence sets and occurrence clauses
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1024,7 +1024,7 @@ Managing the local context
       This notation allows specifying which occurrences of :token:`term` have
       to be substituted in the context. The :n:`in @goal_occurrences` clause
       is an occurrence clause whose syntax and behavior are described in
-      :ref:`goal occurences <occurencessets>`.
+      :ref:`goal occurrences <occurrencessets>`.
 
    .. tacv:: set (@ident @binders := @term) {? in @goal_occurrences }
 
@@ -1509,7 +1509,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
       This syntax is used for selecting which occurrences of :token:`term`
       the case analysis has to be done on. The :n:`in @goal_occurrences`
       clause is an occurrence clause whose syntax and behavior is described
-      in :ref:`occurences sets <occurencessets>`.
+      in :ref:`occurrences sets <occurrencessets>`.
 
    .. tacv:: destruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences }
              edestruct @term {? with @bindings_list } {? as @disj_conj_intro_pattern } {? eqn:@naming_intro_pattern } {? using @term {? with @bindings_list } } {? in @goal_occurrences }
@@ -1659,7 +1659,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
    This syntax is used for selecting which occurrences of :n:`@term` the
    induction has to be carried on. The :n:`in @goal_occurrences` clause is an
    occurrence clause whose syntax and behavior is described in
-   :ref:`occurences sets <occurencessets>`. If variables or hypotheses not
+   :ref:`occurrences sets <occurrencessets>`. If variables or hypotheses not
    mentioning :n:`@term` in their type are listed in :n:`@goal_occurrences`,
    those are generalized as well in the statement to prove.
 
@@ -3513,6 +3513,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
             Info 1 auto with eqdec.
 
    .. cmdv:: Hint Cut @regexp
+      :name: Hint Cut
 
       .. warning::
 
@@ -3546,6 +3547,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       initial cut expression being `emp`.
 
    .. cmdv:: Hint Mode @qualid {* (+ | ! | -)}
+      :name: Hint Mode
 
       This sets an optional mode of use of the identifier :n:`@qualid`. When
       proof-search faces a goal that ends in an application of :n:`@qualid` to
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index be65ff7570..a69cf209c7 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -461,6 +461,7 @@ Requests to the environment
 .. note::
 
    .. table:: Search Blacklist @string
+      :name: Search Blacklist
 
       Specifies a set of strings used to exclude lemmas from the results of :cmd:`Search`,
       :cmd:`SearchHead`, :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries.  A lemma whose
@@ -1200,3 +1201,18 @@ scope of their effect. There are four kinds of commands:
   modifier extends the effect outside the module even when the command
   occurs in a section.  The :cmd:`Set` and :cmd:`Unset` commands belong to this
   category.
+
+.. _exposing-constants-to-ocaml-libraries:
+
+Exposing constants to OCaml libraries
+----------------------------------------------------------------
+
+.. cmd:: Register @qualid__1 as @qualid__2
+
+   This command exposes the constant :n:`@qualid__1` to OCaml libraries under
+   the name :n:`@qualid__2`.  This constant can then be dynamically located
+   calling :n:`Coqlib.lib_ref "@qualid__2"`; i.e., there is no need to known
+   where is the constant defined (file, module, library, etc.).
+
+   Due to its internal nature, this command is not for general use. It is meant
+   to appear only in standard libraries and in support libraries of plug-ins.