Adapt to sub-TOC not showing in PDF output.

9 files changed, 28 insertions, 30 deletions

diff --git a/doc/sphinx/appendix/history-and-changes/index.rst b/doc/sphinx/appendix/history-and-changes/index.rst
index 3535a4d8a7..50ffec8e3f 100644
--- a/doc/sphinx/appendix/history-and-changes/index.rst
+++ b/doc/sphinx/appendix/history-and-changes/index.rst
@@ -5,13 +5,14 @@ History and recent changes
 ==========================
 
 This chapter is divided in two parts.  The first one is about the
-early history of Coq and is presented in chronological order.  The
-second one provides release notes about recent versions of Coq and is
-presented in reverse chronological order.  When updating your copy of
-Coq to a new version (especially a new major version), it is strongly
-recommended that you read the corresponding release notes.  They may
-contain advice that will help you understand the differences with the
-previous version and upgrade your projects.
+:ref:`early history of Coq <history>` and is presented in
+chronological order.  The second one provides :ref:`release notes
+about recent versions of Coq <changes>` and is presented in reverse
+chronological order.  When updating your copy of Coq to a new version
+(especially a new major version), it is strongly recommended that you
+read the corresponding release notes.  They may contain advice that
+will help you understand the differences with the previous version and
+upgrade your projects.
 
 .. toctree::
    :maxdepth: 1
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 6d9979a704..afe22d24e5 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -1,3 +1,5 @@
+.. _changes:
+
 --------------
 Recent changes
 --------------
diff --git a/doc/sphinx/history.rst b/doc/sphinx/history.rst
index c4a48d6985..153dc1f368 100644
--- a/doc/sphinx/history.rst
+++ b/doc/sphinx/history.rst
@@ -1,3 +1,5 @@
+.. _history:
+
 --------------------
 Early history of Coq
 --------------------
diff --git a/doc/sphinx/language/core/index.rst b/doc/sphinx/language/core/index.rst
index c78c0737db..07dcfff444 100644
--- a/doc/sphinx/language/core/index.rst
+++ b/doc/sphinx/language/core/index.rst
@@ -27,8 +27,6 @@ users may rely on external plugins that provide advanced and complex
 tactics without fear of these tactics being buggy, because the kernel
 will have to check their output.
 
-This chapter is divided in several sub-chapters:
-
 .. toctree::
    :maxdepth: 1
 
diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst
index 5b5c2ab737..f22927d627 100644
--- a/doc/sphinx/language/extensions/index.rst
+++ b/doc/sphinx/language/extensions/index.rst
@@ -13,8 +13,6 @@ chapter, we present these language extensions and we give some
 explanations on how this language is translated down to the core
 language presented in the :ref:`previous chapter <core-language>`.
 
-This chapter is divided in several sub-chapters:
-
 .. toctree::
    :maxdepth: 1
 
diff --git a/doc/sphinx/proofs/automatic-tactics/index.rst b/doc/sphinx/proofs/automatic-tactics/index.rst
index e89bde63bc..a219770c69 100644
--- a/doc/sphinx/proofs/automatic-tactics/index.rst
+++ b/doc/sphinx/proofs/automatic-tactics/index.rst
@@ -10,8 +10,6 @@ be used to solve some specific categories of goals, and some
 programmable tactics, that the user can instrument to handle some
 complex goals in new domains.
 
-This chapter is divided in several sub-chapters:
-
 .. toctree::
    :maxdepth: 1
 
diff --git a/doc/sphinx/proofs/creating-tactics/index.rst b/doc/sphinx/proofs/creating-tactics/index.rst
index 5882f10ec3..1af1b0b726 100644
--- a/doc/sphinx/proofs/creating-tactics/index.rst
+++ b/doc/sphinx/proofs/creating-tactics/index.rst
@@ -13,13 +13,6 @@ this has also highlighted its limits and fragility.  The experimental
 language :ref:`Ltac2 <ltac2>` is a typed and more principled variant
 which is more adapted to building complex tactics.
 
-.. toctree::
-   :maxdepth: 1
-
-   ../../proof-engine/ltac
-   ../../proof-engine/ltac2
-
-
 There are other solutions beyond these two tactic languages to write
 new tactics:
 
@@ -33,3 +26,9 @@ new tactics:
   effort and commitment.  A tutorial for writing Coq plugins is
   available in the Coq repository in `doc/plugin_tutorial
   <https://github.com/coq/coq/tree/master/doc/plugin_tutorial>`_.
+
+.. toctree::
+   :maxdepth: 1
+
+   ../../proof-engine/ltac
+   ../../proof-engine/ltac2
diff --git a/doc/sphinx/proofs/writing-proofs/index.rst b/doc/sphinx/proofs/writing-proofs/index.rst
index cc4f7e1305..a279a5957f 100644
--- a/doc/sphinx/proofs/writing-proofs/index.rst
+++ b/doc/sphinx/proofs/writing-proofs/index.rst
@@ -20,9 +20,9 @@ When a proof is complete, the user leaves the proof mode and defers
 the verification of the resulting proof term to the :ref:`kernel
 <core-language>`.
 
-This chapter is divided in several sub-chapters, describing the basic
-ideas of the proof mode (during which tactics can be used), and
-several flavors of tactics, including the SSReflect proof language:
+This chapter is divided in several parts, describing the basic ideas
+of the proof mode (during which tactics can be used), and several
+flavors of tactics, including the SSReflect proof language.
 
 .. toctree::
    :maxdepth: 1
diff --git a/doc/sphinx/using/libraries/index.rst b/doc/sphinx/using/libraries/index.rst
index 2228df5ab8..d0848e6c3f 100644
--- a/doc/sphinx/using/libraries/index.rst
+++ b/doc/sphinx/using/libraries/index.rst
@@ -8,7 +8,13 @@ Coq is distributed with a standard library and a set of internal
 plugins (most of which provide tactics that have already been
 presented in :ref:`writing-proofs`).  This chapter presents this
 standard library and some of these internal plugins which provide
-features that are not tactics:
+features that are not tactics.
+
+In addition, Coq has a rich ecosystem of external libraries and
+plugins.  These libraries and plugins can be browsed online through
+the `Coq Package Index <https://coq.inria.fr/opam/www/>`_ and
+installed with the `opam package manager
+<https://coq.inria.fr/opam-using.html>`_.
 
 .. toctree::
    :maxdepth: 1
@@ -16,9 +22,3 @@ features that are not tactics:
    ../../language/coq-library
    ../../addendum/extraction
    ../../addendum/miscellaneous-extensions
-
-In addition, Coq has a rich ecosystem of external libraries and
-plugins.  These libraries and plugins can be browsed online through
-the `Coq Package Index <https://coq.inria.fr/opam/www/>`_ and
-installed with the `opam package manager
-<https://coq.inria.fr/opam-using.html>`_.