[doc] Work around sphinx-doc/sphinx#4979

doc/sphinx/proof-engine/proof-handling.rst

@@ -405,7 +405,12 @@ The following example script illustrates all these features:
 
    You tried to apply a tactic but no goals were under focus. Using :n:`@bullet` is  mandatory here.
 
-.. exn:: No such goal. Try unfocusing with %{.
+.. FIXME: the :noindex: below works around a Sphinx issue.
+   (https://github.com/sphinx-doc/sphinx/issues/4979)
+   It should be removed once that issue is fixed.
+
+.. exn:: No such goal. Try unfocusing with %}.
+   :noindex:
 
    You just finished a goal focused by ``{``, you must unfocus it with ``}``.
 

doc/tools/coqrst/coqdomain.py

@@ -110,7 +110,9 @@ def _render_signature(self, signature, signode):
         # Explicit object naming
         'name': directives.unchanged,
         # Silence warnings produced by report_undocumented_coq_objects
-        'undocumented': directives.flag
+        'undocumented': directives.flag,
+        # noindex omits this object from its index
+        'noindex': directives.flag
     }
 
     def subdomain_data(self):
@@ -166,18 +168,18 @@ def _add_target(self, signode, name):
 
     def _add_index_entry(self, name, target):
         """Add `name` (pointing to `target`) to the main index."""
-        index_text = name
+        # remove trailing . , found in commands, but not ... (ellipsis)
+        trim = name.endswith(".") and not name.endswith("...")
+        index_text = name[:-1] if trim else 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`."""
+        """Attach a link target to `signode` and an index entry for `name`.
+        This is only called (from ``ObjectDescription.run``) if ``:noindex:`` isn't specified."""
         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