aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-21 19:07:29 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-21 19:07:29 +0200
commit01fcf80e83ff85bf07cd3dc59cadad096b68ac92 (patch)
tree031de4d062639137eb2e98e67c7463b672792a33 /doc
parent4a3697da7be172c1559588d326a2f02c80bb98e9 (diff)
parent7f528cdb0ee42a40792d242357a239969f51cada (diff)
Merge PR #7770: Move indices on top on the TOC. Closes #7764.
Diffstat (limited to 'doc')
-rwxr-xr-xdoc/sphinx/conf.py1
-rw-r--r--doc/sphinx/credits.rst5
-rw-r--r--doc/sphinx/index.rst33
-rw-r--r--doc/sphinx/introduction.rst2
4 files changed, 25 insertions, 16 deletions
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 135c24aed..8127d3df3 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -104,7 +104,6 @@ exclude_patterns = [
'Thumbs.db',
'.DS_Store',
'introduction.rst',
- 'credits.rst',
'README.rst',
'README.template.rst'
]
diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst
index a75659798..2562dec46 100644
--- a/doc/sphinx/credits.rst
+++ b/doc/sphinx/credits.rst
@@ -1,3 +1,8 @@
+.. include:: preamble.rst
+.. include:: replaces.rst
+
+.. _credits:
+
-------------------------------------------
Credits
-------------------------------------------
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index 136f9088b..f3ae49381 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -1,16 +1,31 @@
-.. _introduction:
-
.. include:: preamble.rst
.. include:: replaces.rst
.. include:: introduction.rst
-.. include:: credits.rst
------------------
Table of contents
------------------
.. toctree::
+ :caption: Indexes
+
+ genindex
+ coq-cmdindex
+ coq-tacindex
+ coq-optindex
+ coq-exnindex
+
+.. No entries yet
+ * :index:`thmindex`
+
+.. toctree::
+ :caption: Preamble
+
+ self
+ credits
+
+.. toctree::
:caption: The language
language/gallina-specification-language
@@ -65,18 +80,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
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
index 75ff72c4d..20e4069f4 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -1,3 +1,5 @@
+.. _introduction:
+
------------------------
Introduction
------------------------