aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx/index.rst
diff options
context:
space:
mode:
authorGravatar Laurent Théry <laurent.thery@inria.fr>2018-03-15 14:10:53 +0100
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-04-10 16:33:05 +0200
commit956b36b6313000da84a2e2b241823cce60748daa (patch)
treea86e66864ae212d6ea4235f4b092276493867deb /doc/sphinx/index.rst
parentaf4c91877bb8a34b8f1d0b2c01ed1940ab33514f (diff)
[Sphinx] Add chapter 15
Thanks to Laurent Théry 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 e2824d7ca..e24e6a4ec 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -39,6 +39,7 @@ Table of contents
:caption: Practical tools
practical-tools/coq-commands
+ practical-tools/utilities
practical-tools/coqide
.. toctree::