Commit 2026-10-20 14:09 373becf6
View on Github →chore: remove unused tactics (#45073)
This PR removes/replaces uses of try, all_goals and any_goals that are flagged by the improved unused tactic linter from #44676.
chore: remove unused tactics (#45073)
This PR removes/replaces uses of try, all_goals and any_goals that are flagged by the improved unused tactic linter from #44676.