aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/language')
-rw-r--r--doc/sphinx/language/gallina-specification-language.rst4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index aa41f8058d..4dcd7deb13 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -553,8 +553,8 @@ has type :token:`type`.
.. cmd:: Axiom @ident : @term
- This command links *term* to the name *ident* as its specification in
- the global context. The fact asserted by *term* is thus assumed as a
+ This command links :token:`term` to the name :token:`ident` as its specification in
+ the global context. The fact asserted by :token:`term` is thus assumed as a
postulate.
.. exn:: @ident already exists.