From 805d78d12443d9df646362c024bfa83466c27fdd Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel <clement.pitclaudel@live.com>
Date: Fri, 27 Apr 2018 23:35:40 +0200
Subject: [sphinx] Warn for dangling tacn / cmd / opt / ... references.

---
 doc/tools/coqrst/coqdomain.py | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'doc/tools')

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index f09ed4b55..21093bd90 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -732,14 +732,14 @@ class CoqDomain(Domain):
 
     roles = {
         # Each of these roles lives in a different semantic “subdomain”
-        'cmd': XRefRole(),
-        'tac': XRefRole(),
-        'tacn': XRefRole(),
-        'opt': XRefRole(),
-        'thm': XRefRole(),
-        'prodn' : XRefRole(),
-        'exn': XRefRole(),
-        'warn': XRefRole(),
+        'cmd': XRefRole(warn_dangling=True),
+        'tac': XRefRole(warn_dangling=True),
+        'tacn': XRefRole(warn_dangling=True),
+        'opt': XRefRole(warn_dangling=True),
+        'thm': XRefRole(warn_dangling=True),
+        'prodn' : XRefRole(warn_dangling=True),
+        'exn': XRefRole(warn_dangling=True),
+        'warn': XRefRole(warn_dangling=True),
         # This one is special
         'index': IndexXRefRole(),
         # These are used for highlighting
-- 
cgit v1.2.3