Merge PR #10118: Make progress toward #9411: reject new undefined references.

Reviewed-by: cpitclaudel

1 files changed, 15 insertions, 1 deletions

diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index ec3343dac6..53309cd313 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -181,7 +181,21 @@ suppress_warnings = ["misc.highlighting_failure"]
 todo_include_todos = False
 
 # Extra warnings, including undefined references
-nitpicky = False
+nitpicky = True
+
+nitpick_ignore = [ ('token', token) for token in [
+    'tactic',
+    # 142 occurrences currently sort of defined in the ltac chapter,
+    # but is it the right place?
+    'module',
+    'redexpr',
+    'modpath',
+    'dirpath',
+    'collection',
+    'term_pattern',
+    'term_pattern_string',
+    'command',
+    'symbol' ]]
 
 # -- Options for HTML output ----------------------------------------------