Pierre Vial (Apr 02 2021 at 14:41): Pierre Vial (Apr 02 2021 at 14:41):Hi (this question may be unrelated to VsCoq)
I'm currently using a Coq plugin on VsCoq.
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?
Théo Winterhalter (Apr 02 2021 at 14:43):What if you try to use a bullet? Or Unshelve. ?
Last updated: Apr 19 2024 at 20:01 UTC