aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/index.rst
diff options
context:
space:
mode:
authorThéo Zimmermann2018-04-13 10:32:47 +0200
committerThéo Zimmermann2018-04-13 10:32:47 +0200
commitb68e0b4f9ba37d1c2fa5921e1d934b4b38bfdfe7 (patch)
treea6fcfbb975fe7dd1c4b29bebdbfacb4e300f4807 /doc/sphinx/index.rst
parent43053e7e025e57f00741bcd744c20bc6f2c583af (diff)
parent92c604f8b331c3e202d8477019e183c2cfef9f41 (diff)
Merge PR #7117: Sphinx doc chapter 29
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 15e4ff3bc5..8b1d0e7230 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -59,6 +59,7 @@ Table of contents
addendum/generalized-rewriting
addendum/parallel-proof-processing
addendum/miscellaneous-extensions
+ addendum/universe-polymorphism
.. toctree::
:caption: Reference