From 1be31dea4cfd31522898edc07fee0829fea7c68d Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 19 Mar 2020 15:51:18 +0100
Subject: Adapt to sub-TOC not showing in PDF output.

---
 doc/sphinx/using/libraries/index.rst | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'doc/sphinx/using')

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>`_.
-- 
cgit v1.2.3