Convert syntax extensions chapter to prodn

1 files changed, 0 insertions, 9 deletions

diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 2ed9ec21b3..db1340eacb 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -183,18 +183,9 @@ todo_include_todos = False
 nitpicky = True
 
 nitpick_ignore = [ ('token', token) for token in [
-    'assums',
     'binders',
     'collection',
-    'dirpath',
-    'ind_body',
     'modpath',
-    'module',
-    'simple_tactic',
-    'symbol',
-    'term_pattern',
-    'term_pattern_string',
-    'toplevel_selector',
 ]]
 
 # -- Options for HTML output ----------------------------------------------