diff options
Diffstat (limited to 'doc/sphinx/conf.py')
| -rwxr-xr-x | doc/sphinx/conf.py | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index bce88cebde..e2e37ec438 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -183,11 +183,8 @@ todo_include_todos = False nitpicky = True nitpick_ignore = [ ('token', token) for token in [ - 'tactic', 'induction_clause', - 'conversion', 'where', - 'oriented_rewriter', 'bindings_with_parameters', 'destruction_arg' ]] |