Julin S (Jul 07 2022 at 05:27): Julin S (Jul 07 2022 at 05:27):Maybe a silly question, but is there a way to restart only the current sub-goal in coq?
Restart. restarts the whole proof.
Julin S (Jul 07 2022 at 05:28):And is there an undo tactic that reverses the effect of the most recently applied tactic?
Pierre Castéran (Jul 07 2022 at 06:15):There is a command Undo (not a tactic)
https://coq.inria.fr/refman/proofs/writing-proofs/proof-mode.html#coq:cmd.Undo
Julin S (Jul 07 2022 at 06:21):Thanks!
Julin S (Jul 07 2022 at 06:22):Is it considered part of Vernacular?
Pierre Castéran (Jul 07 2022 at 06:41):According to https://coq.inria.fr/about-coq, looks to be (it helps to build an interactive proof).
But .v files should not contain Undoor 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.
Julin S (Jul 07 2022 at 07:11):That explains the 'Use IDE navigation instead' message coqtop shows on using Undo..
Last updated: Oct 13 2024 at 01:02 UTC