aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/appendix
diff options
context:
space:
mode:
authorClément Pit-Claudel2020-05-02 14:06:49 -0400
committerClément Pit-Claudel2020-05-02 14:06:49 -0400
commit16b2734e050d4c28d5da1a509cd2387cb8cebe6b (patch)
tree30660874fbc98736f1e092b827eaf2a67256c960 /doc/sphinx/appendix
parentf129326d545ae27d362132b279167d119894a992 (diff)
parent90285ff50290a49d20d60ffc59725bf87c6acd14 (diff)
Merge PR #12172: Refactor first chapter: first step, the section on basics.
Ack-by: JasonGross Ack-by: jfehrle
Diffstat (limited to 'doc/sphinx/appendix')
-rw-r--r--doc/sphinx/appendix/indexes/index.rst10
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/sphinx/appendix/indexes/index.rst b/doc/sphinx/appendix/indexes/index.rst
index c8b2cf46dc..7dd0f62a9f 100644
--- a/doc/sphinx/appendix/indexes/index.rst
+++ b/doc/sphinx/appendix/indexes/index.rst
@@ -11,17 +11,17 @@ find what you are looking for.
.. toctree::
- ../../genindex
+ ../../std-glossindex
../../coq-cmdindex
../../coq-tacindex
+ ../../coq-attrindex
../../coq-optindex
../../coq-exnindex
- ../../coq-attrindex
- ../../std-glossindex
+ ../../genindex
For reference, here are direct links to the documentation of:
-- :ref:`flags, options and tables <flags-options-tables>`;
+- :ref:`attributes`
+- :ref:`flags-options-tables`;
- controlling the display of warning messages with the :opt:`Warnings`
option;
-- :ref:`gallina-attributes`.