-
Notifications
You must be signed in to change notification settings - Fork 31
Issues: ejgallego/coq-lsp
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
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
Document outline doesn't work with on-demand checking
kind: bug
Something isn't working
#816
opened Sep 1, 2024 by
Alizter
"printer interrupted" in goal window
kind: bug
Something isn't working
#806
opened Jul 14, 2024 by
Alizter
Heatmap disappears when refocusing tab
kind: bug
Something isn't working
part: client (VSCode)
#805
opened Jul 9, 2024 by
Alizter
Slow goal printing in Coq-HoTT theories/Spaces/No/Core.v
kind: bug
Something isn't working
kind: performance
part: pp printer
#798
opened Jun 27, 2024 by
Alizter
Restarting server resets position of goal window
kind: bug
Something isn't working
part: goals and info panel
[bug] Properly handle proof mode
kind: bug
Something isn't working
kind: upstream
kind: upstream-bug
part: flèche
part: upstream
LSP plugin mangling VSCode/ium Settings file
kind: bug
Something isn't working
kind: HCI design
part: client (VSCode)
part: config
_CoqProject won't be loaded from subdirectory
kind: bug
Something isn't working
#639
opened Jan 16, 2024 by
Alizter
Better copying support
good first issue
Good for newcomers
help wanted
Extra attention is needed
kind: HCI design
part: goals and info panel
#634
opened Jan 9, 2024 by
Alizter
Ltac, Notation and Tactic Notation doesn't appear in the document overview
kind: bug
Something isn't working
[test suite] Check files from upstream on CI
kind: bug
Something isn't working
#630
opened Dec 18, 2023 by
ejgallego
Coq-lsp doesn't work when filename includes a dash
kind: enhancement
New feature or request
kind: upstream
part: documentation
part: upstream
#617
opened Nov 23, 2023 by
amblafont
hovering over record types should display the record
good first issue
Good for newcomers
kind: enhancement
New feature or request
#564
opened Oct 2, 2023 by
Alizter
[goals] Option to hide collapsed goal type display
kind: enhancement
New feature or request
part: goals and info panel
Previous Next
ProTip!
Type g i on any issue or pull request to go back to the issue listing page.