aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--doc/sphinx/using/libraries/funind.rst (renamed from doc/sphinx/language/gallina-extensions.rst)2
-rw-r--r--doc/sphinx/using/libraries/index.rst1
2 files changed, 2 insertions, 1 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/using/libraries/funind.rst
index 6d5791bc19..ed00f3d455 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/using/libraries/funind.rst
@@ -2,7 +2,7 @@ Functional induction
====================
.. _advanced-recursive-functions:
-
+
Advanced recursive functions
----------------------------
diff --git a/doc/sphinx/using/libraries/index.rst b/doc/sphinx/using/libraries/index.rst
index d0848e6c3f..ad10869439 100644
--- a/doc/sphinx/using/libraries/index.rst
+++ b/doc/sphinx/using/libraries/index.rst
@@ -22,3 +22,4 @@ installed with the `opam package manager
../../language/coq-library
../../addendum/extraction
../../addendum/miscellaneous-extensions
+ funind