1 files changed, 8 insertions, 9 deletions
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 867a19efe5..f1dd7479c5 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -183,18 +183,17 @@ todo_include_todos = 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',
+    'command',
+    'dirpath',
+    'modpath',
+    'module',
+    'red_expr',
+    'symbol',
+    'tactic',
     'term_pattern',
     'term_pattern_string',
-    'command',
-    'symbol' ]]
+]]
 
 # -- Options for HTML output ----------------------------------------------