aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/appendix/indexes
diff options
context:
space:
mode:
authorClément Pit-Claudel2020-03-19 18:42:10 -0400
committerClément Pit-Claudel2020-03-19 18:42:10 -0400
commit47d92a69773755e2ad5d5f987f87337fdf7e98d8 (patch)
tree3a074b1269952ef2cbbb4d5fce64531580c61443 /doc/sphinx/appendix/indexes
parent9f680f776140c8b3b8f79013262d5bd73761d571 (diff)
parent1be31dea4cfd31522898edc07fee0829fea7c68d (diff)
Merge PR #11601: [refman] Move chapters into new structure.
Reviewed-by: jfehrle
Diffstat (limited to 'doc/sphinx/appendix/indexes')
-rw-r--r--doc/sphinx/appendix/indexes/index.rst24
1 files changed, 24 insertions, 0 deletions
diff --git a/doc/sphinx/appendix/indexes/index.rst b/doc/sphinx/appendix/indexes/index.rst
new file mode 100644
index 0000000000..a5032ff822
--- /dev/null
+++ b/doc/sphinx/appendix/indexes/index.rst
@@ -0,0 +1,24 @@
+:orphan:
+
+.. _indexes:
+
+========
+Indexes
+========
+
+We provide various specialized indexes that are helpful to quickly
+find what you are looking for.
+
+.. toctree::
+
+ ../../genindex
+ ../../coq-cmdindex
+ ../../coq-tacindex
+ ../../coq-optindex
+ ../../coq-exnindex
+
+For reference, here are direct links to the documentation of:
+
+- :ref:`flags, options and tables <flags-options-tables>`;
+- controlling the display of warning messages with the :opt:`Warnings`
+ option.