diff options
| -rwxr-xr-x | doc/sphinx/conf.py | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index ec3343dac6..53309cd313 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -181,7 +181,21 @@ suppress_warnings = ["misc.highlighting_failure"] todo_include_todos = False # Extra warnings, including undefined references -nitpicky = False +nitpicky = True + +nitpick_ignore = [ ('token', token) for token in [ + 'tactic', + # 142 occurrences currently sort of defined in the ltac chapter, + # but is it the right place? + 'module', + 'redexpr', + 'modpath', + 'dirpath', + 'collection', + 'term_pattern', + 'term_pattern_string', + 'command', + 'symbol' ]] # -- Options for HTML output ---------------------------------------------- |