Hi (this question may be unrelated to VsCoq)
I'm currently using a Coq plugin on
A some point, I'm calling a tactic
fooof this plugin.
Then, in the ProofView window, this is just written "There are unfocused goal", but does not display anything else. That is, I don't see the unfocused goals. Moroever,
Show Proofdoes not work, because the state of the proof is huge and use very bureaucratic encodings.
Is there a way to just simply display unfocused goals on
VsCoqor in general?
What if you try to use a bullet? Or
Last updated: Jan 30 2023 at 18:04 UTC