diff options
| author |  Clément Pit-Claudel <clement.pitclaudel@live.com> | 2018-05-04 19:02:11 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel <clement.pitclaudel@live.com> | 2018-05-15 12:05:44 -0400 |
| commit | d5bb8a4ae2f509532ecfb4a53bb91c64d992c2e6 (patch) | |
| tree | 6cf4a3d6bcb485265340dad79dc6f4698342f1ca /doc/sphinx/language/gallina-specification-language.rst | |
| parent | a6545a120c6587af38883597d20ac28131b813a9 (diff) | |
[doc] Address feedback on doc writer guide
Co-Authored-By: @Zimmi48
Diffstat (limited to 'doc/sphinx/language/gallina-specification-language.rst')
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 4 |
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 aa41f8058..4dcd7deb1 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. |