search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
335 stars 68 forks source link

"There are shelved goals. Try using unshelved" #851

Closed TheoWinterhalter closed 2 months ago

TheoWinterhalter commented 2 months ago

When closing a subgoal that leaves shelved goals, the message is

There are shelved goals. Try using unshelved

Besides the missing period, shouldn't it be Unshelve without the d and with a capital U?