From 6a3586d80dd068c2067a8e47effed8122d0bd3b3 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 3 Dec 2020 10:33:33 +0100
Subject: [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.
---
 doc/sphinx/language/core/assumptions.rst | 2 +-
 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.
-- 
cgit v1.2.3