Fix comment.

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>

Remove note about Sphinx tradition.

1 files changed, 1 insertions, 10 deletions

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 5b0f87adfc..b0bbbf33b3 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -220,7 +220,7 @@ class CoqObject(ObjectDescription):
         self.indexnode['entries'].append(('single', index_text, target, '', None))
 
     def add_target_and_index(self, names, _, signode):
-        """Attach a link target to `signode` and an index entries for `names`.
+        """Attach a link target to `signode` and index entries for `names`.
         This is only called (from ``ObjectDescription.run``) if ``:noindex:`` isn't specified."""
         if names:
             for name in names:
@@ -235,15 +235,6 @@ class CoqObject(ObjectDescription):
 
         A node may have either one signature with no name, multiple signatures
         with one name per signatures, or one signature with multiple names.
-
-        (That last case isn't ideal; in the Sphinx tradition, it would be better
-        to have one signature per name, like this:
-
-        .. cmd:: Definition …
-                 Fact …
-                 Lemma …
-                 …
-           :name: Definition; Fact; Lemma; …)
         """
         sigs = self.get_signatures()
         names = self.options.get("name")