aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/language')
-rw-r--r--doc/sphinx/language/gallina-extensions.rst2
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index d618d90ad2..68066faa30 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -2109,6 +2109,8 @@ case, this latter type is considered).
Adds blocks of implicit types with different specifications.
+.. _implicit-generalization:
+
Implicit generalization
~~~~~~~~~~~~~~~~~~~~~~~