aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx/index.rst
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-11 00:33:46 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-12 17:26:35 +0100
commitb00563550b983e81a9949c1e53849f8a21ee307d (patch)
tree2042f457392fa437f95c19b5aa972f910721c534 /doc/sphinx/index.rst
parentb97c80a39bb3471ae681fe5f5afef8a973e4c606 (diff)
[Sphinx] Add table of contents
Diffstat (limited to 'doc/sphinx/index.rst')
-rw-r--r--doc/sphinx/index.rst29
1 files changed, 29 insertions, 0 deletions
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index e69de29bb..0de75ca0c 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -0,0 +1,29 @@
+------------------
+Table of contents
+------------------
+
+.. toctree::
+ :caption: The language
+
+.. toctree::
+ :caption: The proof engine
+
+.. toctree::
+ :caption: User extensions
+
+.. toctree::
+ :caption: Practical tools
+
+.. toctree::
+ :caption: Addendum
+
+.. toctree::
+ :caption: Reference
+ :titlesonly:
+
+.. toctree::
+ :caption: Indexes
+ :titlesonly:
+
+.. No entries yet
+ * :index:`thmindex`