Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#2690)
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 May 15, 2020
1 parent 471d29e commit a4266a0
Showing 1 changed file with 0 additions and 31 deletions.
31 changes: 0 additions & 31 deletions scripts/nolints.txt
Original file line number Diff line number Diff line change
Expand Up @@ -2767,37 +2767,6 @@ apply_nolint tactic.rewrite_all.tracked_rewrite.replace_target doc_blame
apply_nolint tactic.rewrite_all.tracked_rewrite.replace_target_lhs doc_blame
apply_nolint tactic.rewrite_all.tracked_rewrite.replace_target_rhs doc_blame

-- tactic/ring.lean
apply_nolint tactic.interactive.ring.mode doc_blame
apply_nolint tactic.ring.add_atom doc_blame
apply_nolint tactic.ring.cache doc_blame
apply_nolint tactic.ring.cache.cs_app doc_blame
apply_nolint tactic.ring.eval doc_blame
apply_nolint tactic.ring.eval' doc_blame
apply_nolint tactic.ring.eval_add doc_blame
apply_nolint tactic.ring.eval_atom doc_blame
apply_nolint tactic.ring.eval_const_mul doc_blame
apply_nolint tactic.ring.eval_horner doc_blame
apply_nolint tactic.ring.eval_mul doc_blame
apply_nolint tactic.ring.eval_neg doc_blame
apply_nolint tactic.ring.eval_pow doc_blame
apply_nolint tactic.ring.get_atom doc_blame
apply_nolint tactic.ring.get_cache doc_blame
apply_nolint tactic.ring.get_transparency doc_blame
apply_nolint tactic.ring.horner doc_blame
apply_nolint tactic.ring.horner_expr doc_blame
apply_nolint tactic.ring.horner_expr.e doc_blame
apply_nolint tactic.ring.horner_expr.pp doc_blame
apply_nolint tactic.ring.horner_expr.refl_conv doc_blame
apply_nolint tactic.ring.horner_expr.to_string doc_blame
apply_nolint tactic.ring.horner_expr.xadd' doc_blame
apply_nolint tactic.ring.lift doc_blame
apply_nolint tactic.ring.normalize doc_blame
apply_nolint tactic.ring.normalize_mode doc_blame
apply_nolint tactic.ring.ring_m doc_blame
apply_nolint tactic.ring.ring_m.mk_app doc_blame
apply_nolint tactic.ring.ring_m.run doc_blame

-- tactic/ring2.lean
apply_nolint conv.interactive.ring2 doc_blame
apply_nolint tactic.ring2.horner_expr.add doc_blame
Expand Down

0 comments on commit a4266a0

Please sign in to comment.