Commit 2020-12-15 17:57 78e48c02

ci(lint-copy-mod-doc.py): add reserved notation and set_option linters, enable small_alpha_vrachy_check linter (#5330) As requested on Zulip, the reserved notation linter checks for reserve or precedence at the start of a non-comment, non-string literal line in any file other than tactic.core. The new set_option linter disallows set_option pp, set_option profiler and set_option trace at the start of a non-comment, non-string literal line. I also noticed that the small_alpha_vrachy_check linter added in #4802 wasn't actually called, so I added it to the main lint function.