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)

https://coq.inria.fr/refman/proofs/writing-proofs/proof-mode.html#coq:cmd.Undo

Thanks!

Is it considered part of Vernacular?

According to https://coq.inria.fr/about-coq, looks to be (it helps to build an interactive proof).

But `.v`

files should not contain `Undo`

or `Restart`

commands (except for a docmentation purpose).

In Proof General, for instance, I use cursor movements for undoing proof parts, and the saved `.v`

is clean from such commands.

That explains the 'Use IDE navigation instead' message coqtop shows on using `Undo.`

.

Last updated: Jun 25 2024 at 14:01 UTC