Documentation

CustomPrelude.Linter.Syntax.GoalSelector

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.