Maybe a silly question, but is there a way to restart only the current sub-goal in coq?
Restart. restarts the whole proof.
And is there an undo tactic that reverses the effect of the most recently applied tactic?
There is a command
Undo (not a tactic)
Is it considered part of Vernacular?
According to https://coq.inria.fr/about-coq, looks to be (it helps to build an interactive proof).
.v files should not contain
Restart commands (except for a docmentation purpose).
In Proof General, for instance, I use cursor movements for undoing proof parts, and the saved
.vis clean from such commands.
That explains the 'Use IDE navigation instead' message coqtop shows on using
Last updated: Jan 29 2023 at 01:02 UTC