Hi new Zulip user here :) I am not sure if this is the correct format and place to ask questions but here I am :)

I am wondering how to let my customized plugin command "start a new proof/goal"?

My current way of developing plugins is to translate my command into *vernac_expr* and invoke *Vernacinterp.interp*. This works fine and satisfies most of my needs, but when I use the same idea to translate my command into *VernacStartTheoremProof* (which should correspond to using *Theorem* command), the interp function finished successfully but my VsCoq interface didn't enter the proof mode *(as far as it looks like, I am not sure if there is any display error by VsCoq; I also tried to input Qed but it does error with the message "No Focused Proof....")*

Looking forward to any suggestions! I guess there are some plugins that can enter the proof mode but I don't know where to find them :) Great Thanks!

you need to classify as vtstartproof in your mlg

something like this https://github.com/coq/coq/blob/58465d29ec8154af22e8e9a394502288a72b71e7/plugins/ltac/g_obligations.mlg#L86-L90

(the CLASSIFIED BY part)

Gaëtan Gilbert said:

something like this https://github.com/coq/coq/blob/58465d29ec8154af22e8e9a394502288a72b71e7/plugins/ltac/g_obligations.mlg#L86-L90

Thanks for the help! I will try to transplant this example into mine :)

Last updated: Feb 06 2023 at 18:03 UTC