chore(scripts): update nolints.txt (#17008)

I am happy to remove some nolints for you!
leanprover-community · Oct 16, 2022 · 6568f2f · 6568f2f
1 parent 71a759b
commit 6568f2f
Showing 1 changed file with 0 additions and 5 deletions.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -137,11 +137,6 @@ apply_nolint tactic.interactive.traverse_constructor unused_arguments
 apply_nolint tactic.interactive.traverse_field unused_arguments
 apply_nolint tactic.interactive.with_prefix doc_blame
 
--- data/finset/noncomm_prod.lean
-apply_nolint add_monoid_hom.pi_ext fintype_finite
-apply_nolint finset.noncomm_prod_union_of_disjoint to_additive_doc
-apply_nolint monoid_hom.pi_ext fintype_finite
-
 -- data/finsupp/pwo.lean
 apply_nolint finsupp.is_pwo fintype_finite