aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx/index.rst
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-15 09:44:52 +0100
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-04-10 19:23:07 +0200
commitb3142348f10909cac621370297608b2c14b8f1b5 (patch)
treefd8fcd8026a0c116b12156d03c95ac3d72f2df9b /doc/sphinx/index.rst
parent8fbe7741c3e374a2a15adf68a59824f4190b7e20 (diff)
[Sphinx] Add chapter 6
Thanks to Yves Bertot for porting this chapter.
Diffstat (limited to 'doc/sphinx/index.rst')
-rw-r--r--doc/sphinx/index.rst1
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index e24e6a4ec..15e4ff3bc 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -24,6 +24,7 @@ Table of contents
.. toctree::
:caption: The proof engine
+ proof-engine/vernacular-commands
proof-engine/proof-handling
proof-engine/tactics
proof-engine/detailed-tactic-examples