aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx/index.rst
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-15 09:32:26 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-15 14:46:51 +0100
commite3750fc9b94f003ea9b9474345925e7f6fcf57de (patch)
tree5d72460929a2d2f989ddb813df7741cea2792c03 /doc/sphinx/index.rst
parenta8839f8646ae0675361483e99c0b937a6b83bfbe (diff)
[Sphinx] Add chapter 3
Thanks to Pierre Letouzey 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 84c670175..b3f160df1 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -17,6 +17,7 @@ Table of contents
:caption: The language
language/gallina-extensions
+ language/coq-library
language/cic
language/module-system