linter.fugue.selectorTry #
all: try tac — and every other selector over a bare try (1-3: try tac,
all_goals try tac) — runs tac under try, so a goal where tac fails is silently left
untouched and the proof no longer records which goals the selector closed. Name the goals the
tactic applies to (1,3: tac), or drop the try and the selector both if it closes them all.