diff options
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/core/assumptions.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/core/definitions.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/arguments-command.rst | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst index e029068630..e86a6f4a67 100644 --- a/doc/sphinx/language/core/assumptions.rst +++ b/doc/sphinx/language/core/assumptions.rst @@ -170,7 +170,7 @@ has type :n:`@type`. Axiom R_S_inv : forall x y, R x y <-> S y x. .. exn:: @ident already exists. - :name: @ident already exists. (Axiom) + :name: ‘ident’ already exists. (Axiom) :undocumented: .. warn:: @ident is declared as a local axiom diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index ec5b896dab..6da1f90ecb 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -109,7 +109,7 @@ Section :ref:`typing-rules`. .. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. .. exn:: @ident already exists. - :name: @ident already exists. (Definition) + :name: ‘ident’ already exists. (Definition) :undocumented: .. exn:: The term @term has type @type while it is expected to have type @type'. @@ -170,7 +170,7 @@ Chapter :ref:`Tactics`. The basic assertion command is: :undocumented: .. exn:: @ident already exists. - :name: @ident already exists. (Theorem) + :name: ‘ident’ already exists. (Theorem) The name you provided is already defined. You have then to choose another name. diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst index 95c5914e47..d178311b4c 100644 --- a/doc/sphinx/language/extensions/arguments-command.rst +++ b/doc/sphinx/language/extensions/arguments-command.rst @@ -79,7 +79,7 @@ Setting properties of a function's arguments `!` the function will be unfolded only if all the arguments marked with `!` - evaulate to constructors. See :ref:`Args_effect_on_unfolding`. + evaluate to constructors. See :ref:`Args_effect_on_unfolding`. :n:`@name {? % @scope }` a *formal parameter* of the function :n:`@reference` (i.e. |