aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/appendix
diff options
context:
space:
mode:
authorClément Pit-Claudel2020-04-02 17:18:30 -0400
committerClément Pit-Claudel2020-04-02 17:18:30 -0400
commit4950d9631383acc5c4383d9c6d0a597f8d3206b3 (patch)
treef27b37d9d0f46237631f54d1eec142196a1aadc7 /doc/sphinx/appendix
parent1806d3f6d43020c3219186416b4c63e80af2f11c (diff)
parent9df2a43d5336ceb67a8da45f7b64c074b090790f (diff)
Merge PR #11869: Add an index for attributes.
Reviewed-by: cpitclaudel
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`.