Stream: VsCoq devs & users

Topic: Show unfocused goal


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

view this post on Zulip Théo Winterhalter (Apr 02 2021 at 14:43):

What if you try to use a bullet? Or Unshelve. ?


Last updated: Jan 30 2023 at 18:04 UTC