Fix auto-completion

[arnoudvanderleer]

Note: I am still on v0.3.8, so not entirely sure how this translates to the new version. I am not sure how hard this is to implement (although I guess it would be pretty hard). Would it be possible to have VScoq autocomplete / -suggest names of lemmas and/or variables that are in scope? At some point, the names of my own lemmas get very long, or I forget the exact wording of a lemma in some file that I import. Would it be possible to have VScoq try to autocomplete the names of these lemmas when I am typing?

[rtetley]

You should test the latest version (vscoq2) which has an experimental option to do just that ! Just don't forget to toggle the completion setting which is disabled by default :-)

[tcosmo]

Hello!

I toggled the option on the latest version of VsCoq using vscode 1.89.0 on a MacBook Pro M3 Max with Sonoma 14.2.1

But I get:

"[Error - 21:10:07] Request textDocument/completion failed. Message: Can't get completions Code: -32803 "