diff options
| author | Théo Zimmermann | 2020-12-03 10:33:33 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-12-03 11:33:31 +0100 |
| commit | 6a3586d80dd068c2067a8e47effed8122d0bd3b3 (patch) | |
| tree | 5ecc00b955a9d3a1492fa8d0e441fb27a7e2126a | |
| parent | a88568e751d63d8db93450213272c8b28928dbf2 (diff) | |
[refman] Fix error names.
The @ syntax is not supported in the name, so we transform it manually
as it would have been if no name had been provided.
| -rw-r--r-- | doc/sphinx/language/core/assumptions.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/core/definitions.rst | 4 |
2 files changed, 3 insertions, 3 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. |