aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language/extensions/index.rst
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/language/extensions/index.rst')
-rw-r--r--doc/sphinx/language/extensions/index.rst2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst
index ea7271179e..ed207ca743 100644
--- a/doc/sphinx/language/extensions/index.rst
+++ b/doc/sphinx/language/extensions/index.rst
@@ -4,7 +4,7 @@
Language extensions
===================
-Elaboration extends the language accepted by the |Coq| kernel to make it
+Elaboration extends the language accepted by the Coq kernel to make it
easier to use. For example, this lets the user omit most type
annotations because they can be inferred, call functions with implicit
arguments which will be inferred as well, extend the syntax with