1 files changed, 20 insertions, 11 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index c9487abf03..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
 
@@ -449,7 +454,7 @@ def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]):
        it names the introduced hypothesis :token:`ident`.
 
     Note that this example also uses ``:token:``.  That's because ``ident`` is
-    defined in the the Coq manual as a grammar production, and ``:token:``
+    defined in the Coq manual as a grammar production, and ``:token:``
     creates a link to that.  When referring to a placeholder that happens to be
     a grammar production, ``:token:`…``` is typically preferable to ``:n:`@…```.
     """
@@ -571,6 +576,9 @@ class ExampleDirective(BaseAdmonition):
     http://docutils.sourceforge.net/docs/ref/rst/directives.html#generic-admonition
     for more details.
 
+    Optionally, any text immediately following the ``.. example::`` header is
+    used as the example's title.
+
     Example::
 
        .. example:: Adding a hint to a database
@@ -583,13 +591,14 @@ class ExampleDirective(BaseAdmonition):
     """
     node_class = nodes.admonition
     directive_name = "example"
+    optional_arguments = 1
 
     def run(self):
         # ‘BaseAdmonition’ checks whether ‘node_class’ is ‘nodes.admonition’,
         # and uses arguments[0] as the title in that case (in other cases, the
         # title is unset, and it is instead set in the HTML visitor).
-        assert not self.arguments # Arguments have been parsed as content
-        self.arguments = ['Example']
+        assert len(self.arguments) <= 1
+        self.arguments = [": ".join(['Example'] + self.arguments)]
         self.options['classes'] = ['admonition', 'note']
         return super().run()