From aee50066c9ef94ec2967e2f6f659ecb7a0f9598e Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 25 Jul 2018 15:08:33 +0200
Subject: [sphinx] Add a way of skipping names in the indexes.

---
 doc/tools/coqrst/coqdomain.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/tools')

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))
 
-- 
cgit v1.2.3