diff options
| author | coqbot-app[bot] | 2020-12-03 19:25:25 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-03 19:25:25 +0000 |
| commit | 632b960ada4392ddd8be6f2e49caab46b93c022f (patch) | |
| tree | 68873105244017ded126a01e4e4a2eb1e0a99675 | |
| parent | afbc39d8c4f24e2e8ccda0fcb861fb947f3f4c71 (diff) | |
| parent | 6a3586d80dd068c2067a8e47effed8122d0bd3b3 (diff) | |
Merge PR #13558: [refman] Fix error names.
Reviewed-by: jfehrle
| -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. |