Skip to content

Commit

Permalink
chore(scripts): update nolints.txt (#2862)
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 30, 2020
1 parent f95e809 commit 5455fe1
Showing 1 changed file with 0 additions and 4 deletions.
4 changes: 0 additions & 4 deletions scripts/nolints.txt
Expand Up @@ -178,7 +178,6 @@ apply_nolint ring_hom.to_add_monoid_hom doc_blame
apply_nolint ring_hom.to_monoid_hom doc_blame
apply_nolint semiring doc_blame
apply_nolint sub_mul def_lemma doc_blame
apply_nolint zero_ne_one_class doc_blame

-- algebraic_geometry/presheafed_space.lean
apply_nolint algebraic_geometry.PresheafedSpace has_inhabited_instance
Expand Down Expand Up @@ -1394,8 +1393,6 @@ apply_nolint polynomial.eval_sub_factor doc_blame
apply_nolint polynomial.eval₂_zero unused_arguments
apply_nolint polynomial.lcoeff doc_blame
apply_nolint polynomial.mod doc_blame
apply_nolint polynomial.nonzero_comm_ring.of_polynomial_ne doc_blame
apply_nolint polynomial.nonzero_comm_semiring.of_polynomial_ne doc_blame
apply_nolint polynomial.pow_add_expansion doc_blame
apply_nolint polynomial.pow_sub_pow_factor doc_blame
apply_nolint polynomial.rec_on_horner doc_blame
Expand Down Expand Up @@ -2024,7 +2021,6 @@ apply_nolint ideal.is_prime doc_blame
apply_nolint ideal.quotient doc_blame has_inhabited_instance
apply_nolint ideal.quotient.map_mk doc_blame
apply_nolint ideal.quotient.mk doc_blame
apply_nolint ideal.quotient.nonzero_comm_ring doc_blame
apply_nolint ideal.span doc_blame
apply_nolint is_local_ring doc_blame
apply_nolint is_local_ring_hom doc_blame
Expand Down

0 comments on commit 5455fe1

Please sign in to comment.