Stream: Coq users

Topic: Restart current sub-goal


view this post on Zulip 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.

view this post on Zulip Julin S (Jul 07 2022 at 05:28):

And is there an undo tactic that reverses the effect of the most recently applied tactic?

view this post on Zulip 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

view this post on Zulip Julin S (Jul 07 2022 at 06:21):

Thanks!

view this post on Zulip Julin S (Jul 07 2022 at 06:22):

Is it considered part of Vernacular?

view this post on Zulip 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.

view this post on Zulip Julin S (Jul 07 2022 at 07:11):

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


Last updated: Jan 29 2023 at 01:02 UTC