diff --git a/scripts/nolints.txt b/scripts/nolints.txt index fbe4573b539aa..c8ebcda676a9d 100644 --- a/scripts/nolints.txt +++ b/scripts/nolints.txt @@ -464,9 +464,8 @@ apply_nolint fin2.elim0 doc_blame -- data/fintype/basic.lean apply_nolint finset.insert_none doc_blame -apply_nolint fintype.bij_inv unused_arguments apply_nolint fintype.choose doc_blame -apply_nolint fintype.choose_x doc_blame unused_arguments +apply_nolint fintype.choose_x doc_blame apply_nolint fintype.fintype_prod_left doc_blame apply_nolint fintype.fintype_prod_right doc_blame apply_nolint fintype.of_injective doc_blame