From b6cfffeb940b93d1bf20c0068a0da69fc3024bab Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Sun, 21 Apr 2019 23:03:39 -0700 Subject: Remove duplicate copy of _warn_if_duplicate_name. --- doc/tools/coqrst/coqdomain.py | 7 ------- 1 file changed, 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 -- cgit v1.2.3