From 7a57a23e4fb8a74e8746d4eaee900f2ced37a28a Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 9 Aug 2020 14:25:51 -0700
Subject: Convert misc chapters to prodn

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

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

diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index a8a574c861..75ac2a76cd 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -183,9 +183,7 @@ todo_include_todos = False
 nitpicky = True
 
 nitpick_ignore = [ ('token', token) for token in [
-    'collection',
     'tactic',
-    'bindings',
     'induction_clause',
     'conversion',
     'where',
-- 
cgit v1.2.3