rename linter

Author: datokrat

src/Lean/Linter/Coe.lean

@@ -39,7 +39,7 @@ def coercionsBannedInCore : List Name := [``optionCoe, ``instCoeSubarrayArray]
 def coeLinter : Linter where
   run := fun _ => do
     let mainModule ← getMainModule
-    let isCoreModule := mainModule = `lean.run.coeLinter ∨ (mainModule.getRoot ∈ [`Init, `Std])
+    let isCoreModule := mainModule = `lean.run.linterCoe ∨ (mainModule.getRoot ∈ [`Init, `Std])
     let shouldWarnOnDeprecated := getLinterValue linter.deprecatedCoercions (← getLinterOptions)
     let trees ← Elab.getInfoTrees
     for tree in trees do

tests/lean/run/coeLinter.lean tests/lean/run/linterCoe.leantests/lean/run/coeLinter.lean renamed to tests/lean/run/linterCoe.lean

@@ -1,7 +1,7 @@
 module
 
 -- by default, linters are disabled when running tests
-set_option linter.deprecatedCoercions true
+set_option linter.all true
 
 structure X
 structure Y
@@ -27,6 +27,7 @@ Note: This linter can be disabled with `set_option linter.deprecatedCoercions fa
 #guard_msgs in
 def h (foo : X) : Y := foo
 
+/-- -/
 notation a " +' " b => a + b
 
 @[deprecated "" (since := "")]