aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/appendix
diff options
context:
space:
mode:
authorThéo Zimmermann2020-05-01 13:22:42 +0200
committerThéo Zimmermann2020-05-01 18:00:12 +0200
commit90285ff50290a49d20d60ffc59725bf87c6acd14 (patch)
treef4e765e15738c0c69114cac9739ed55854c1120d /doc/sphinx/appendix
parentff5320974f8008f48dc15b89f01c6e6162780928 (diff)
Move essential vocabulary and syntax conventions to section on basics.
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`.