Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Query shortcuts don't work for symbols highlighted in proof view #283

Open
MSoegtropIMC opened this issue Mar 9, 2022 · 1 comment
Open
Labels
enhancement New feature or request

Comments

@MSoegtropIMC
Copy link

In CoqIDE I am frequently using the "Check" or "Print" shortcut on symbols in the proof view. It is not that uncommon that after simplification or unfolding one has symbols in the proof view which are no where in the proof (so far).

In VsCoq the "Check" and "Print" shortcuts apparently do not work if a symbol is selected in proof view.

@MSoegtropIMC
Copy link
Author

Btw.: they don't work for symbols in the ourput pane either. E frequently use Print recursively in CoqIDE, that is I select a symbol in the output of Pint and use the Print shortcut again. This does not work in VsCoq - I need to copy and paste the symbol into the .v file buffer.

@maximedenes maximedenes added this to the 2.0.0+beta1 milestone Feb 6, 2023
@maximedenes maximedenes removed this from the 2.0.0+beta1 milestone Jul 31, 2023
@rtetley rtetley added the enhancement New feature or request label Jan 17, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

3 participants