search

coq / vscoq

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

'Coq: Display Goals' resulted in an error #837

Closed motiwalam closed 2 months ago

motiwalam commented 2 months ago

I get the following 'extension.coq.displayGoals' not found error when trying to use the "Coq: Display Goals" command:

image

Nothing shows up in the "Extension Host" logs in VSCode. I've tried uninstalling everything and reinstalling but that doesn't work. All of the other Coq commands visible in the command palette seem to work fine.

Can't find anything about other people having this problem, so I'm not sure if this is some issue with my environment.

rtetley commented 2 months ago

This is because the Coq: Display goals command was removed, I should remove it from the manifest ! Just to be sure, what is your use case for this command ? Maybe we should put it back.

motiwalam commented 2 months ago

Ah, okay. I thought this command was the way to open the goals panel but I was mistaken; I see it just opens automatically once you start interpreting. Sorry about that!