Skip to content

Commit 2012f87

Browse files
committed
try simp_all? is not required anymore
1 parent b1793a3 commit 2012f87

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Mathlib/Tactic/TacticAnalysis/Declarations.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -360,7 +360,7 @@ register_option linter.tacticAnalysis.tryAtEachStepSimpAllSuggestions : Bool :=
360360

361361
@[tacticAnalysis linter.tacticAnalysis.tryAtEachStepSimpAllSuggestions,
362362
inherit_doc linter.tacticAnalysis.tryAtEachStepSimpAllSuggestions]
363-
def tryAtEachStepSimpAllSuggestions := tryAtEachStep fun _ _ => `(tactic| try simp_all? +suggestions)
363+
def tryAtEachStepSimpAllSuggestions := tryAtEachStep fun _ _ => `(tactic| simp_all? +suggestions)
364364

365365
-- /-- Run `canonical +suggestions` at every step in proofs, reporting where it succeeds. -/
366366
-- register_option linter.tacticAnalysis.tryAtEachStepCanonicalSuggestions : Bool := {

0 commit comments

Comments
 (0)