14 files changed, 128 insertions, 80 deletions
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..57f1174d59 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
@@ -116,7 +120,7 @@ G. Dowek, allowed hierarchical developments of mathematical theories.
 This high-level language was called the *Mathematical Vernacular*.
 Furthermore, an interactive *Theorem Prover* permitted the incremental
 construction of proof trees in a top-down manner, subgoaling recursively
-and backtracking from dead-alleys. The theorem prover executed tactics
+and backtracking from dead-ends. The theorem prover executed tactics
 written in CAML, in the LCF fashion. A basic set of tactics was
 predefined, which the user could extend by his own specific tactics.
 This system (Version 4.10) was released in 1989. Then, the system was
@@ -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/cic.rst b/doc/sphinx/language/cic.rst
index 381f8bb661..835d6dcaa6 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -533,10 +533,10 @@ Convertibility
 Let us write :math:`E[Γ] ⊢ t \triangleright u` for the contextual closure of the
 relation :math:`t` reduces to :math:`u` in the global environment
 :math:`E` and local context :math:`Γ` with one of the previous
-reductions β, ι, δ or ζ.
+reductions β, δ, ι or ζ.
 
 We say that two terms :math:`t_1` and :math:`t_2` are
-*βιδζη-convertible*, or simply *convertible*, or *equivalent*, in the
+*βδιζη-convertible*, or simply *convertible*, or *equivalent*, in the
 global environment :math:`E` and local context :math:`Γ` iff there
 exist terms :math:`u_1` and :math:`u_2` such that :math:`E[Γ] ⊢ t_1 \triangleright
 … \triangleright u_1` and :math:`E[Γ] ⊢ t_2 \triangleright … \triangleright u_2` and either :math:`u_1` and
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 8c82526f0c..1a33a9a46e 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1112,6 +1112,59 @@ co-inductive definitions are also allowed.
    object of type :g:`(EqSt s1 s2)`. We will see how to introduce infinite
    objects in Section :ref:`cofixpoint`.
 
+Caveat
+++++++
+
+The ability to define co-inductive types by constructors, hereafter called
+*positive co-inductive types*, is known to break subject reduction. The story is
+a bit long: this is due to dependent pattern-matching which implies
+propositional η-equality, which itself would require full η-conversion for
+subject reduction to hold, but full η-conversion is not acceptable as it would
+make type-checking undecidable.
+
+Since the introduction of primitive records in Coq 8.5, an alternative
+presentation is available, called *negative co-inductive types*. This consists
+in defining a co-inductive type as a primitive record type through its
+projections. Such a technique is akin to the *co-pattern* style that can be
+found in e.g. Agda, and preserves subject reduction.
+
+The above example can be rewritten in the following way.
+
+.. coqtop:: all
+
+   Set Primitive Projections.
+   CoInductive Stream : Set := Seq { hd : nat; tl : Stream }.
+   CoInductive EqSt (s1 s2: Stream) : Prop := eqst {
+     eqst_hd : hd s1 = hd s2;
+     eqst_tl : EqSt (tl s1) (tl s2);
+   }.
+
+Some properties that hold over positive streams are lost when going to the
+negative presentation, typically when they imply equality over streams.
+For instance, propositional η-equality is lost when going to the negative
+presentation. It is nonetheless logically consistent to recover it through an
+axiom.
+
+.. coqtop:: all
+
+   Axiom Stream_eta : forall s: Stream, s = cons (hs s) (tl s).
+
+More generally, as in the case of positive coinductive types, it is consistent
+to further identify extensional equality of coinductive types with propositional
+equality:
+
+.. coqtop:: all
+
+   Axiom Stream_ext : forall (s1 s2: Stream), EqSt s1 s2 -> s1 = s2.
+
+As of Coq 8.9, it is now advised to use negative co-inductive types rather than
+their positive counterparts.
+
+.. seealso::
+   :ref:`primitive_projections` for more information about negative
+   records and primitive projections.
+
+
 Definition of recursive functions
 ---------------------------------
 
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/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 46851050ac..741f9fe5b0 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -144,8 +144,9 @@ list of assertion commands is given in :ref:`Assertions`. The command
    the proof is a subset of the declared one.
 
    The set of declared variables is closed under type dependency. For
-   example if ``T`` is variable and a is a variable of type ``T``, the commands
-   ``Proof using a`` and ``Proof using T a`` are actually equivalent.
+   example, if ``T`` is a variable and ``a`` is a variable of type
+   ``T``, then the commands ``Proof using a`` and ``Proof using T a``
+   are equivalent.
 
    .. cmdv:: Proof using {+ @ident } with @tactic
 
@@ -632,16 +633,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/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 52609546d5..3ca0ffe678 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -916,11 +916,8 @@ but also folds ``x`` in the goal.
      .. coqtop:: reset
 
         From Coq Require Import ssreflect.
-        Set Implicit Arguments.
-        Unset Strict Implicit.
-        Unset Printing Implicit Defensive.
 
-     .. coqtop:: all undo
+     .. coqtop:: all
 
         Lemma test x t (Hx : x = 3) : x + t = 4.
         set z := 3 in Hx.
@@ -929,6 +926,10 @@ If the localization also mentions the goal, then the result is the following one
 
   .. example::
 
+     .. coqtop:: reset
+
+        From Coq Require Import ssreflect.
+
      .. coqtop:: all
 
         Lemma test x t (Hx : x = 3) : x + t = 4.
@@ -2485,8 +2486,7 @@ destruction of existential assumptions like in the tactic:
   .. coqtop:: all
 
      Lemma test : True.
-     have [x Px]: exists x : nat, x > 0.
-     Focus 2.
+     have [x Px]: exists x : nat, x > 0; last first.
 
 An alternative use of the ``have`` tactic is to provide the explicit proof
 term for the intermediate lemma, using tactics of the form:
@@ -2564,8 +2564,7 @@ copying the goal itself.
   .. coqtop:: all
 
      Lemma test : True.
-     have suff H : 2 + 2 = 3.
-     Focus 2.
+     have suff H : 2 + 2 = 3; last first.
 
   Note that H is introduced in the second goal.
 
@@ -2852,8 +2851,7 @@ pattern will be used to process its instance.
   .. coqtop:: all
 
      Lemma simple n (ngt0 : 0 < n ) : P n.
-     gen have ltnV, /andP[nge0 neq0] : n ngt0 / (0 <= n) && (n != 0).
-     Focus 2.
+     gen have ltnV, /andP[nge0 neq0] : n ngt0 / (0 <= n) && (n != 0); last first.
 
 
 .. _advanced_generalization_ssr:
@@ -3556,6 +3554,7 @@ corresponding new goals will be generated.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
+     Set Warnings "-notation-overridden".
 
   .. coqtop:: all
 
@@ -3756,9 +3755,10 @@ which the function is supplied:
    :name: congr
 
 This tactic:
-+ checks that the goal is a Leibniz equality
-+ matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints.
-+ generates the subgoals corresponding to pairwise equalities of the arguments present in the goal.
+
+   + checks that the goal is a Leibniz equality;
+   + matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints;
+   + generates the subgoals corresponding to pairwise equalities of the arguments present in the goal.
 
 The goal can be a non dependent product ``P -> Q``. In that case, the
 system asserts the equation ``P = Q``, uses it to solve the goal, and
@@ -4918,7 +4918,7 @@ which produces the converse implication. In both cases, the two
 first Prop arguments are implicit.
 
 If ``term`` is an instance of the ``reflect`` predicate, then ``A`` will be one
-of the defined view hints for the ``reflec``t predicate, which are by
+of the defined view hints for the ``reflect`` predicate, which are by
 default the ones present in the file ``ssrbool.v``. These hints are not
 only used for choosing the appropriate direction of the translation,
 but they also allow complex transformation, involving negations.
@@ -4933,9 +4933,9 @@ but they also allow complex transformation, involving negations.
      Unset Printing Implicit Defensive.
      Section Test.
 
-  .. coqtop:: in
+  .. coqtop:: all
 
-     Lemma introN : forall (P : Prop) (b : bool), reflect P b -> ~ P -> ~~b.
+     Check introN.
 
   .. coqtop:: all
 
@@ -4945,12 +4945,11 @@ but they also allow complex transformation, involving negations.
   In fact this last script does not
   exactly use the hint ``introN``, but the more general hint:
 
-  .. coqtop:: in
+  .. coqtop:: all
 
-     Lemma introNTF : forall (P : Prop) (b c : bool),
-       reflect P b -> (if c then ~ P else P) -> ~~ b = c.
+     Check introNTF.
 
-  The lemma ` `introN`` is an instantiation of introNF using c := true.
+  The lemma ``introN`` is an instantiation of ``introNF`` using ``c := true``.
 
 Note that views, being part of :token:`i_pattern`, can be used to interpret
 assertions too. For example the following script asserts ``a && b`` but
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 125c4c25a3..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