diff options
Diffstat (limited to 'doc/sphinx/conf.py')
| -rwxr-xr-x | doc/sphinx/conf.py | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index f1dd7479c5..22102aa3ab 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -108,7 +108,7 @@ master_doc = "index" # General information about the project. project = 'Coq' -copyright = '1999-2019, Inria, CNRS and contributors' +copyright = '1999-2020, Inria, CNRS and contributors' author = 'The Coq Development Team' # The version info for the project you're documenting, acts as replacement for @@ -183,16 +183,21 @@ todo_include_todos = False nitpicky = True nitpick_ignore = [ ('token', token) for token in [ + 'binders', 'collection', 'command', + 'definition', 'dirpath', + 'inductive', + 'ind_body', 'modpath', 'module', - 'red_expr', + 'simple_tactic', 'symbol', 'tactic', 'term_pattern', 'term_pattern_string', + 'toplevel_selector', ]] # -- Options for HTML output ---------------------------------------------- |