[sphinx] Add a way of skipping names in the indexes.

3 files changed, 3 insertions, 3 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index 32de15ee31..30ac2cec80 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/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index c9487abf03..8f135c9185 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -158,7 +158,7 @@ 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:
+        if self.index_suffix and not name.startswith("_"):
             index_text += " " + self.index_suffix
         self.indexnode['entries'].append(('single', index_text, target, '', None))