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

I am happy to remove some nolints for you!
leanprover-community · Apr 10, 2020 · ebdeb3b · ebdeb3b
1 parent 29080c8
commit ebdeb3b
Showing 1 changed file with 0 additions and 4 deletions.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -1796,9 +1796,6 @@ apply_nolint set.bUnion_eq_sigma_of_disjoint doc_blame
 apply_nolint set.seq doc_blame
 apply_nolint set.sigma_to_Union doc_blame
 
--- data/setoid.lean
-apply_nolint setoid.is_partition doc_blame
-
 -- data/string/basic.lean
 apply_nolint string.ltb doc_blame
 
@@ -2267,7 +2264,6 @@ apply_nolint well_founded.succ doc_blame
 apply_nolint well_founded.sup doc_blame
 
 -- order/bounded_lattice.lean
-apply_nolint with_bot doc_blame
 apply_nolint with_top doc_blame
 
 -- order/complete_lattice.lean