aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/using/libraries/index.rst
diff options
context:
space:
mode:
authorClément Pit-Claudel2020-04-03 10:40:44 -0400
committerClément Pit-Claudel2020-04-03 10:40:44 -0400
commita37814ae4df4a97c0b5bdbef68d72e52412e5467 (patch)
tree3fa57e6194514a93ac5479d3bb54264e70f07997 /doc/sphinx/using/libraries/index.rst
parentacefe58cd39c9a4efee632f7f92f56fb4d5285bb (diff)
parentcf978356dd0791cf6b4bc90dcc07a91cd57bd79e (diff)
Merge PR #11914: Start the split of the Gallina Extensions chapter.
Reviewed-by: jfehrle
Diffstat (limited to 'doc/sphinx/using/libraries/index.rst')
-rw-r--r--doc/sphinx/using/libraries/index.rst1
1 files changed, 1 insertions, 0 deletions
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