Merge PR #8170: Don't index names starting with `_` in docs

4 files changed, 17 insertions, 13 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 2264b170fc..4673107e3d 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -32,7 +32,7 @@ Names (link targets) are auto-generated for most simple objects, though they can
 - Vernacs (commands) have their name set to the first word of their signature.  For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```.
 - Vernac variants, tactic notations, and tactic variants do not have a default name.
 
-Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms).  Undocumented objects should have the `:undocumented:` flag instead, as shown above.  When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects)::
+Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms).  Undocumented objects should have the `:undocumented:` flag instead, as shown above.  When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes)::
 
    .. cmdv:: Lemma @ident {? @binders} : @type
              Remark @ident {? @binders} : @type
diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst
index f1d2541eb6..c333d6e9d5 100644
--- a/doc/sphinx/README.template.rst
+++ b/doc/sphinx/README.template.rst
@@ -32,7 +32,7 @@ Names (link targets) are auto-generated for most simple objects, though they can
 - Vernacs (commands) have their name set to the first word of their signature.  For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```.
 - Vernac variants, tactic notations, and tactic variants do not have a default name.
 
-Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms).  Undocumented objects should have the `:undocumented:` flag instead, as shown above.  When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects)::
+Most objects should have a body (i.e. a block of indented text following the signature, called “contents” in Sphinx terms).  Undocumented objects should have the `:undocumented:` flag instead, as shown above.  When multiple objects have a single description, they can be grouped into a single object, like this (semicolons can be used to separate the names of the objects; names starting with ``_`` will be omitted from the indexes)::
 
    .. cmdv:: Lemma @ident {? @binders} : @type
              Remark @ident {? @binders} : @type
diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
index 344134b6f9..72dd79d930 100644
--- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst
+++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
@@ -473,9 +473,8 @@ corresponding left-hand side and call yourself recursively on sub-
 terms. If there is no match, we are at a leaf: return the
 corresponding constructor (here ``f_const``) applied to the term.
 
-.. exn:: quote: not a simple fixpoint
-
-   Happens when ``quote`` is not able to perform inversion properly.
+When ``quote`` is not able to perform inversion properly, it will error out with
+:exn:`quote: not a simple fixpoint`.
 
 
 Introducing variables map
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index a0dc16aac7..40554c3ca3 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -123,7 +123,13 @@ class CoqObject(ObjectDescription):
         """
         self._render_annotation(signode)
         self._render_signature(signature, signode)
-        return self._names.get(signature) or self._name_from_signature(signature)
+        name = self._names.get(signature)
+        if name is None:
+            name = self._name_from_signature(signature)
+            # remove trailing ‘.’ found in commands, but not ‘...’ (ellipsis)
+            if name is not None and name.endswith(".") and not name.endswith("..."):
+                name = name[:-1]
+        return name
 
     def _warn_if_duplicate_name(self, objects, name):
         """Check that two objects in the same domain don't have the same name."""
@@ -157,18 +163,17 @@ class CoqObject(ObjectDescription):
 
     def _add_index_entry(self, name, target):
         """Add `name` (pointing to `target`) to the main index."""
-        index_text = name
-        if self.index_suffix:
-            index_text += " " + self.index_suffix
-        self.indexnode['entries'].append(('single', index_text, target, '', None))
+        assert isinstance(name, str)
+        if not name.startswith("_"):
+            index_text = name
+            if self.index_suffix:
+                index_text += " " + self.index_suffix
+            self.indexnode['entries'].append(('single', index_text, target, '', None))
 
     def add_target_and_index(self, name, _, signode):
         """Attach a link target to `signode` and an index entry for `name`."""
         if name:
             target = self._add_target(signode, name)
-            # remove trailing . , found in commands, but not ... (ellipsis)
-            if name[-1] == "." and not name[-3:] == "..." :
-                name = name[0:-1]
             self._add_index_entry(name, target)
             return target