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

1 files changed, 1 insertions, 1 deletions

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))