aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx/index.rst
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-13 17:27:11 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-15 14:18:44 +0100
commit5a86c2264e24347c0a17bfe1adab05e0315f3992 (patch)
tree20ebde25f16e3f0162d47b3e128d1d531df38174 /doc/sphinx/index.rst
parentb40a567d88a0fff6afe6c96c07d555d820d49fe8 (diff)
[Sphinx] Add chapter 8
Thanks to Heiko Becker and Nikita Zyuzin for porting this chapter.
Diffstat (limited to 'doc/sphinx/index.rst')
-rw-r--r--doc/sphinx/index.rst2
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index a83312d33..f8f7a9ed9 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -23,6 +23,8 @@ Table of contents
.. toctree::
:caption: The proof engine
+ proof-engine/tactics
+
.. toctree::
:caption: User extensions