Two more

leanprover-community · Oct 31, 2024 · 69bd919 · 69bd919
1 parent 737eda7
commit 69bd919
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 1 deletion.
diff --git a/Mathlib/Tactic/DeclarationNames.lean b/Mathlib/Tactic/DeclarationNames.lean
@@ -6,7 +6,9 @@ Authors: Damiano Testa, Moritz Firsching
 
 import Lean.DeclarationRange
 import Lean.ResolveName
--- transitively imported in Mathlib.Init
+-- Import this linter explicitly to ensure that
+-- this file has a valid copyright header and module docstring.
+import Mathlib.Tactic.Linter.Header
 
 /-!
 This file contains functions that are used by multiple linters.

diff --git a/Mathlib/Tactic/Finiteness/Attr.lean b/Mathlib/Tactic/Finiteness/Attr.lean
@@ -4,6 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 import Aesop
+-- Import this linter explicitly to ensure that
+-- this file has a valid copyright header and module docstring.
+import Mathlib.Tactic.Linter.Header
 
 /-! # Finiteness tactic attribute -/