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

I am happy to remove some nolints for you!
leanprover-community · Apr 11, 2020 · 83359d1 · 83359d1
1 parent 4fa2924
commit 83359d1
Showing 1 changed file with 0 additions and 8 deletions.
diff --git a/scripts/nolints.txt b/scripts/nolints.txt
@@ -730,14 +730,6 @@ apply_nolint category_theory.sum.associativity doc_blame
 apply_nolint category_theory.sum.associator doc_blame
 apply_nolint category_theory.sum.inverse_associator doc_blame
 
--- category_theory/types.lean
-apply_nolint category_theory.functor.sections doc_blame
-apply_nolint category_theory.hom_of_element doc_blame
-apply_nolint category_theory.iso.to_equiv doc_blame
-apply_nolint category_theory.ulift_functor doc_blame
-apply_nolint category_theory.ulift_trivial doc_blame
-apply_nolint equiv.to_iso doc_blame
-
 -- category_theory/whiskering.lean
 apply_nolint category_theory.functor.associator doc_blame
 apply_nolint category_theory.functor.left_unitor doc_blame