Merge PR #7606: Allow more than one signature and name per Sphinx object

1 files changed, 15 insertions, 1 deletions

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 8d6e23764f..ab3a485b22 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -118,7 +118,7 @@ class CoqObject(ObjectDescription):
             annotation = self.annotation + ' '
             signode += addnodes.desc_annotation(annotation, annotation)
         self._render_signature(signature, signode)
-        return self.options.get("name") or self._name_from_signature(signature)
+        return self._names.get(signature) or self._name_from_signature(signature)
 
     def _record_name(self, name, target_id):
         """Record a name, mapping it to target_id
@@ -176,8 +176,22 @@ class CoqObject(ObjectDescription):
             if report == "warning":
                 raise self.warning(msg)
 
+    def _prepare_names(self):
+        sigs = self.get_signatures()
+        names = self.options.get("name")
+        if names is None:
+            self._names = {}
+        else:
+            names = [n.strip() for n in names.split(";")]
+            if len(names) != len(sigs):
+                ERR = ("Expected {} semicolon-separated names, got {}.  " +
+                       "Please provide one name per signature line.")
+                raise self.error(ERR.format(len(names), len(sigs)))
+            self._names = dict(zip(sigs, names))
+
     def run(self):
         self._warn_if_undocumented()
+        self._prepare_names()
         return super().run()
 
 class PlainObject(CoqObject):