1 files changed, 6 insertions, 1 deletions
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 77cb3ecc21..22102aa3ab 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -183,16 +183,21 @@ todo_include_todos = False
 nitpicky = True
 
 nitpick_ignore = [ ('token', token) for token in [
+    'binders',
     'collection',
     'command',
+    'definition',
     'dirpath',
+    'inductive',
+    'ind_body',
     'modpath',
     'module',
-    'red_expr',
+    'simple_tactic',
     'symbol',
     'tactic',
     'term_pattern',
     'term_pattern_string',
+    'toplevel_selector',
 ]]
 
 # -- Options for HTML output ----------------------------------------------