From 0b5251ee8a6f69d4b0700991884e68dfdfcf8ad6 Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Fri, 18 May 2018 01:10:15 -0400
Subject: [doc] Rewrite and document the prodn directive

It was broken and undocumented. We dropped the git logs, too, so it wasn't clear
who wrote it and why it was introduced in the first place.
---
 doc/tools/coqrst/coqdomain.py | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 6317e6e214..2bf9776751 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -149,6 +149,13 @@ 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