diff options
| author | Maxime Dénès | 2018-06-21 19:07:29 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-06-21 19:07:29 +0200 |
| commit | 01fcf80e83ff85bf07cd3dc59cadad096b68ac92 (patch) | |
| tree | 031de4d062639137eb2e98e67c7463b672792a33 /doc/sphinx | |
| parent | 4a3697da7be172c1559588d326a2f02c80bb98e9 (diff) | |
| parent | 7f528cdb0ee42a40792d242357a239969f51cada (diff) | |
Merge PR #7770: Move indices on top on the TOC. Closes #7764.
Diffstat (limited to 'doc/sphinx')
| -rwxr-xr-x | doc/sphinx/conf.py | 1 | ||||
| -rw-r--r-- | doc/sphinx/credits.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/index.rst | 33 | ||||
| -rw-r--r-- | doc/sphinx/introduction.rst | 2 |
4 files changed, 25 insertions, 16 deletions
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 135c24aed9..8127d3df3f 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 a756597986..2562dec468 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 136f9088b1..f3ae493817 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 75ff72c4da..20e4069f45 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -1,3 +1,5 @@ +.. _introduction: + ------------------------ Introduction ------------------------ |