Skip to content

Pull requests: ejgallego/coq-lsp

New pull request New
28 Open 688 Closed
28 Open 688 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

[fleche] [io] [nit] Improve logging for unexpected feedback. kind: internal part: Coq API part: flèche
#1000 opened Jul 25, 2025 by ejgallego Loading… 0.2.4
[lsp] Return executed sentence info in goal request. kind: enhancement New feature or request lsp: goals needs: test-case part: lsp server part: protocol (custom)
#999 opened Jul 24, 2025 by jpoiret Loading… 0.2.4
1
3
Adapt to rocq-prover/rocq#20962 (LStream.next returns option)
#998 opened Jul 23, 2025 by SkySkimmer • Draft
Adapt to rocq-prover/rocq#20917 (ltac_use_default is CAst) kind: overlay kind: upstream part: serlib part: upstream
#997 opened Jul 21, 2025 by SkySkimmer • Draft 0.2.4
Adapt to rocq-prover/rocq#20926 (notations code movement) kind: overlay kind: upstream part: serlib part: upstream
#996 opened Jul 18, 2025 by SkySkimmer • Draft 0.2.4
Configurable completion chars kind: enhancement New feature or request kind: HCI design lsp: completion
#993 opened Jul 12, 2025 by Durbatuluk1701 Loading… 0.2.4
@ejgallego
3
[petanque] Implement petanque/definition kind: enhancement New feature or request part: petanque
#984 opened Jun 20, 2025 by ejgallego • Draft 0.2.4
[goaldump] Also serialize goals in sexp format.
#975 opened Jun 4, 2025 by ejgallego • Draft
Adapt to rocq-prover/rocq#20506 kind: overlay kind: upstream part: serlib part: upstream
#945 opened Apr 14, 2025 by jrosain Loading…
Add LaTeX to the layout engine
#878 opened Dec 2, 2024 by patrick-nicodemus • Draft 0.2.4
Adapt to Coq PR #19301: unify the syntax of definition and theorem
#869 opened Oct 23, 2024 by herbelin Loading…
Adapt to coq/coq#19023 (Vernacexpr.subproof_kind) kind: overlay kind: upstream part: serlib
#866 opened Oct 22, 2024 by SkySkimmer • Draft 0.2.4
Adapt to Coq PR #19404: an algebra of types for the instances of notation variables
#810 opened Jul 21, 2024 by herbelin Loading…
[plugins] Baseline plugin for fcc
#799 opened Jul 1, 2024 by ejgallego • Draft 0.2.5
[petanque] Allow clients to set file contents
#790 opened Jun 13, 2024 by ejgallego • Draft 0.2.5
[tools] Checkdecls tool for Coq blueprints
#785 opened Jun 12, 2024 by ejgallego Loading… 0.2.5
[layout engine] Move Coq Layout engine tree to coq-lsp repos. kind: enhancement New feature or request part: pp printer
#668 opened Apr 4, 2024 by ejgallego • Draft 0.2.4
[wip] File auto-build kind: enhancement New feature or request needs: test-case needs: testing part: compiler part: flèche part: workspace setup
#641 opened Jan 19, 2024 by ejgallego • Draft 0.2.5
1
[example] Example how to use the LSP client
#626 opened Nov 28, 2023 by ejgallego • Draft 0.2.4
Add Emacs mode. needs: changes entry part: client (Emacs)
#592 opened Nov 1, 2023 by arthuraa Loading… 0.3.0
2
[hover] [wip] First prototype of show documentation on hover
#590 opened Oct 26, 2023 by ejgallego • Draft
2
[workspace] Include list of known modules in workspace. kind: enhancement New feature or request part: lsp server part: workspace setup
#505 opened Jun 20, 2023 by ejgallego • Draft 0.2.4
[Nix] build without submodules
#372 opened Feb 17, 2023 by Alizter • Draft
5
[lsp] Preliminary support for pull diagnostics
#361 opened Feb 16, 2023 by ejgallego • Draft
2
[goals] [wip] Show info waiting
#216 opened Jan 22, 2023 by ejgallego • Draft 0.3.0
ProTip! Adding no:label will show everything without a label.