diff --git a/scripts/nolints.txt b/scripts/nolints.txt index abb2c3e2b1e8f..d7464a01aeb33 100644 --- a/scripts/nolints.txt +++ b/scripts/nolints.txt @@ -389,32 +389,6 @@ apply_nolint stream.unfolds doc_blame -- data/stream/init.lean apply_nolint stream.is_bisimulation doc_blame --- deprecated/group.lean -apply_nolint is_group_hom.comp to_additive_doc -apply_nolint is_group_hom.id to_additive_doc -apply_nolint is_group_hom.injective_iff to_additive_doc -apply_nolint is_group_hom.inv to_additive_doc -apply_nolint is_group_hom.map_inv to_additive_doc -apply_nolint is_group_hom.map_one to_additive_doc -apply_nolint is_group_hom.mk' to_additive_doc -apply_nolint is_group_hom.mul to_additive_doc -apply_nolint is_group_hom.to_is_monoid_hom to_additive_doc -apply_nolint is_monoid_hom.comp to_additive_doc -apply_nolint is_monoid_hom.id to_additive_doc -apply_nolint is_monoid_hom.inv to_additive_doc -apply_nolint is_monoid_hom.map_mul to_additive_doc -apply_nolint is_mul_hom.inv to_additive_doc -apply_nolint is_mul_hom.mul to_additive_doc -apply_nolint is_mul_hom.to_is_monoid_hom to_additive_doc -apply_nolint mul_equiv.is_monoid_hom to_additive_doc -apply_nolint mul_equiv.is_mul_hom to_additive_doc - --- deprecated/subfield.lean -apply_nolint is_subfield doc_blame - --- deprecated/subring.lean -apply_nolint ring.closure doc_blame - -- group_theory/coset.lean apply_nolint subgroup.card_subgroup_dvd_card to_additive_doc diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt index bf4a542d5bb7f..444e14b351eba 100644 --- a/scripts/style-exceptions.txt +++ b/scripts/style-exceptions.txt @@ -27,8 +27,6 @@ src/data/seq/computation.lean : line 12 : ERR_MOD : Module docstring missing, or src/data/seq/parallel.lean : line 14 : ERR_MOD : Module docstring missing, or too late src/data/seq/seq.lean : line 11 : ERR_MOD : Module docstring missing, or too late src/data/seq/wseq.lean : line 10 : ERR_MOD : Module docstring missing, or too late -src/deprecated/subfield.lean : line 8 : ERR_MOD : Module docstring missing, or too late -src/deprecated/subring.lean : line 10 : ERR_MOD : Module docstring missing, or too late src/logic/relator.lean : line 11 : ERR_MOD : Module docstring missing, or too late src/meta/coinductive_predicates.lean : line 8 : ERR_MOD : Module docstring missing, or too late src/tactic/apply_fun.lean : line 8 : ERR_MOD : Module docstring missing, or too late