feat: show message when goals are unfocused

coq / vscoq

Visual Studio Code extension for Coq

MIT License

335 stars 68 forks source link

feat: show message when goals are unfocused #901

Closed rtetley closed 3 weeks ago

rtetley commented 4 weeks ago

When there are unfocused goals (when bullets are used) we now display a message stating the subproof is complete but there are still unfocused goals. Closes #643