aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/appendix
diff options
context:
space:
mode:
authorThéo Zimmermann2020-03-20 17:57:28 +0100
committerThéo Zimmermann2020-03-20 18:00:06 +0100
commit9df2a43d5336ceb67a8da45f7b64c074b090790f (patch)
tree7ec47696ac7bf03d7fea5ee7815e9aaf48db7805 /doc/sphinx/appendix
parent4d025d4161599ea20cd1dbf489a6412f019a7a7e (diff)
Add an index for attributes.
Diffstat (limited to 'doc/sphinx/appendix')
-rw-r--r--doc/sphinx/appendix/indexes/index.rst4
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/sphinx/appendix/indexes/index.rst b/doc/sphinx/appendix/indexes/index.rst
index a5032ff822..2ece726df7 100644
--- a/doc/sphinx/appendix/indexes/index.rst
+++ b/doc/sphinx/appendix/indexes/index.rst
@@ -16,9 +16,11 @@ find what you are looking for.
../../coq-tacindex
../../coq-optindex
../../coq-exnindex
+ ../../coq-attrindex
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.
+ option;
+- :ref:`gallina-attributes`.