diff options
Diffstat (limited to 'doc/sphinx/conf.py')
| -rwxr-xr-x | doc/sphinx/conf.py | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 99762c7a0e..ee8784fc02 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -187,6 +187,16 @@ nitpick_ignore = [ ('token', token) for token in [ 'collection', 'modpath', 'tactic', + 'destruction_arg', + 'bindings', + 'induction_clause', + 'conversion', + 'where', + 'oriented_rewriter', + 'hintbases', + 'bindings_with_parameters', + 'destruction_arg', + 'clause_dft_concl' ]] # -- Options for HTML output ---------------------------------------------- |