From d9ab85ffae85e756b2ed94c3b3fe655d3b541aaf Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Tue, 3 Mar 2020 10:23:15 -0800
Subject: Remove some productionlists

---
 doc/sphinx/conf.py | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'doc/sphinx/conf.py')

diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 22102aa3ab..d864f8549d 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -183,9 +183,9 @@ todo_include_todos = False
 nitpicky = True
 
 nitpick_ignore = [ ('token', token) for token in [
+    'assums',
     'binders',
     'collection',
-    'command',
     'definition',
     'dirpath',
     'inductive',
@@ -194,7 +194,6 @@ nitpick_ignore = [ ('token', token) for token in [
     'module',
     'simple_tactic',
     'symbol',
-    'tactic',
     'term_pattern',
     'term_pattern_string',
     'toplevel_selector',
-- 
cgit v1.2.3