Commit 2025-11-04 18:11 86a00bdf

View on Github →

feat(TacticAnalysis): check if we are in a try/anyGoals context (#29964) This PR adds a check if the tactic is being run in a try or anyGoals call, so that we do not add a warning for the original tactic failing in this context. This was the source of a few "original tactic failed" in the grind regression reports.

Estimated changes

Modified Mathlib/Tactic/TacticAnalysis.lean

added structure Mathlib.TacticAnalysis.TacticNode

modified def Mathlib.TacticAnalysis.findTacticSeqs

modified def Mathlib.TacticAnalysis.runPass

Modified Mathlib/Tactic/TacticAnalysis/Declarations.lean

Modified MathlibTest/TacticAnalysis.lean

added theorem create_a_few_goals