If the current goals are
g₁ ⋯ gᵢ ⋯ gₙ,
splitGoalsAndGetNth i returns
(gᵢ, [g₁, ⋯, gᵢ₋₁], [gᵢ₊₁, ⋯, gₙ]).
reverse is passed as
i-th goal is picked by counting backwards.
splitGoalsAndGetNth 1 true puts the last goal in the first component
of the returned term.
on_goal n => tacSeq creates a block scope for the
n-th goal and tries the sequence
tacSeq on it.
on_goal -n => tacSeq does the same, but the
n-th goal is chosen by counting from the
The goal is not required to be solved and any resulting subgoals are inserted back into the list of goals, replacing the chosen goal.