diff options
| author | Maxime Dénès | 2018-05-16 15:25:07 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-05-16 15:25:07 +0200 |
| commit | 19e24bf1f5eefee37ee2648c04844b5ea3ca2ab2 (patch) | |
| tree | 60ae3d8527f10aa5e198639139364bdaebddf821 /doc/sphinx/language | |
| parent | 3f480c993311d19b152deb6bb4dc561188d76fc7 (diff) | |
| parent | e266976abc8c170c1e4bf1c98629c190b844f1ab (diff) | |
Merge PR #7391: Add a small documentation writer's guide
Diffstat (limited to 'doc/sphinx/language')
| -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 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. |