diff options
| author | Théo Zimmermann | 2020-03-19 15:51:18 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-03-19 15:51:27 +0100 |
| commit | 1be31dea4cfd31522898edc07fee0829fea7c68d (patch) | |
| tree | 3bb6df49147fbb96603f950d922d153feccc27d7 /doc/sphinx/using | |
| parent | f5be988da566d0a48c67bd81be6d32376b3ba2a5 (diff) | |
Adapt to sub-TOC not showing in PDF output.
Diffstat (limited to 'doc/sphinx/using')
| -rw-r--r-- | doc/sphinx/using/libraries/index.rst | 14 |
1 files changed, 7 insertions, 7 deletions
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>`_. |