aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-06-10 21:50:39 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-06-17 12:48:26 +0200
commitb22595da96013de18f4a2bab5e6333d75a650554 (patch)
tree5a61ed6c9b0aff1899273f6c6345d2ec78ccd136 /doc/sphinx
parent9f8345d6bddfe2965ef9dc0155092348d5166f51 (diff)
Move indexes on top on the TOC. Closes #7764.
Diffstat (limited to 'doc/sphinx')
-rw-r--r--doc/sphinx/index.rst24
1 files changed, 12 insertions, 12 deletions
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index 136f9088b..bd3bd93dd 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -11,6 +11,18 @@ Table of contents
------------------
.. toctree::
+ :caption: Indexes
+
+ genindex
+ coq-cmdindex
+ coq-tacindex
+ coq-optindex
+ coq-exnindex
+
+.. No entries yet
+ * :index:`thmindex`
+
+.. toctree::
:caption: The language
language/gallina-specification-language
@@ -65,18 +77,6 @@ Table of contents
zebibliography
-.. toctree::
- :caption: Indexes
-
- genindex
- coq-cmdindex
- coq-tacindex
- coq-optindex
- coq-exnindex
-
-.. No entries yet
- * :index:`thmindex`
-
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