aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language/coq-library.rst
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/language/coq-library.rst')
-rw-r--r--doc/sphinx/language/coq-library.rst2
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index 6af6e78972..afb49413dd 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -200,6 +200,8 @@ The following abbreviations are allowed:
The type annotation ``:A`` can be omitted when ``A`` can be
synthesized by the system.
+.. _coq-equality:
+
Equality
++++++++