Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#2482)
Browse files Browse the repository at this point in the history
I am happy to remove some nolints for you!
  • Loading branch information
leanprover-community-bot committed Apr 21, 2020
1 parent ffa97d0 commit 585d77a
Showing 1 changed file with 0 additions and 37 deletions.
37 changes: 0 additions & 37 deletions scripts/nolints.txt
Original file line number Diff line number Diff line change
Expand Up @@ -3119,43 +3119,6 @@ apply_nolint transfer.analyse_decls doc_blame
apply_nolint transfer.compute_transfer doc_blame

-- tactic/where.lean
apply_nolint lean.parser.get_includes doc_blame
apply_nolint lean.parser.get_namespace doc_blame
apply_nolint lean.parser.get_variables doc_blame
apply_nolint where.binder_less_important doc_blame
apply_nolint where.binder_priority doc_blame
apply_nolint where.collect_by doc_blame
apply_nolint where.collect_by_aux doc_blame
apply_nolint where.collect_implicit_names doc_blame
apply_nolint where.compile_variable_list doc_blame
apply_nolint where.fetch_potential_variable_names doc_blame
apply_nolint where.find_var doc_blame
apply_nolint where.format_variable doc_blame
apply_nolint where.get_all_in_namespace doc_blame
apply_nolint where.get_def_variables doc_blame
apply_nolint where.get_includes_core doc_blame
apply_nolint where.get_namespace_core doc_blame
apply_nolint where.get_opens doc_blame
apply_nolint where.get_variables_core doc_blame
apply_nolint where.inflate doc_blame
apply_nolint where.is_in_namespace_nonsynthetic doc_blame
apply_nolint where.is_variable_name doc_blame
apply_nolint where.mk_flag doc_blame
apply_nolint where.resolve_var doc_blame
apply_nolint where.resolve_vars doc_blame
apply_nolint where.resolve_vars_aux doc_blame
apply_nolint where.select_for_which doc_blame
apply_nolint where.sort_variable_list doc_blame
apply_nolint where.strip_namespace doc_blame
apply_nolint where.strip_pi_binders doc_blame
apply_nolint where.strip_pi_binders_aux doc_blame
apply_nolint where.trace_end doc_blame
apply_nolint where.trace_includes doc_blame
apply_nolint where.trace_namespace doc_blame
apply_nolint where.trace_nl doc_blame
apply_nolint where.trace_opens doc_blame
apply_nolint where.trace_variables doc_blame
apply_nolint where.trace_where doc_blame
apply_nolint where.where_cmd unused_arguments

-- tactic/wlog.lean
Expand Down

0 comments on commit 585d77a

Please sign in to comment.