Merge PR #9978: Remove duplicate copy of _warn_if_duplicate_name.

Reviewed-by: SkySkimmer

1 files changed, 0 insertions, 7 deletions

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index eaf1b2c2ad..0ade9fdbf5 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -149,13 +149,6 @@ class CoqObject(ObjectDescription):
             msg = MSG.format(name, self.env.doc2path(objects[name][0]))
             self.state_machine.reporter.warning(msg, line=self.lineno)
 
-    def _warn_if_duplicate_name(self, objects, name):
-        """Check that two objects in the same domain don't have the same name."""
-        if name in objects:
-            MSG = 'Duplicate object: {}; other is at {}'
-            msg = MSG.format(name, self.env.doc2path(objects[name][0]))
-            self.state_machine.reporter.warning(msg, line=self.lineno)
-
     def _record_name(self, name, target_id):
         """Record a name, mapping it to target_id