linter.fugue.goalSelector #
CustomPrelude's Rocq-style tac_selector covers what all_goals / on_goal do and more:
all: tac, 3: tac, 1,3-5,9-12: tac, also in conv. any_goals is useless — drop it.
linter.fugue.goalSelector #CustomPrelude's Rocq-style tac_selector covers what all_goals / on_goal do and more:
all: tac, 3: tac, 1,3-5,9-12: tac, also in conv. any_goals is useless — drop it.