issues
search
ejgallego
/
coq-lsp
Visual Studio Code Extension and Language Server Protocol for Coq
GNU Lesser General Public License v2.1
143
stars
31
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
[parsing] Bump Coq to fix lexer error recovery.
#665
ejgallego
closed
5 months ago
0
[perf] [code] Fix Coq perf view display.
#664
ejgallego
closed
5 months ago
0
[bug] The selectionRange request only returns the range of one position of the sent positions
#663
driverag22
closed
5 months ago
6
[memo] Cache control and eviction improvements
#662
ejgallego
closed
5 months ago
0
[coq] Monitor Coq calls under a `token` interruption parameter.
#661
ejgallego
closed
5 months ago
0
[coq] Adapt `Coq.Protect` interface to incorporate an interruption token
#660
ejgallego
closed
5 months ago
1
Adapt to coq/coq#18422 (indirect accessor handled through vernactypes)
#659
SkySkimmer
closed
5 months ago
0
[dev] [opam] Bump Dune dev version to 3.13
#658
ejgallego
closed
5 months ago
0
[vendor] Bump Coq and SerAPI
#657
ejgallego
closed
5 months ago
0
[bug] Properly handle proof mode
#656
ejgallego
opened
5 months ago
0
Add request to vizcar extension
#655
bhaktishh
closed
5 months ago
0
Adding definition kind LetContext
#654
herbelin
closed
5 months ago
2
Improvement for goal display
#652
qcfu-bu
opened
6 months ago
2
[ci] [v8.19] Try to make CI green again.
#651
ejgallego
closed
6 months ago
7
[fcc] Add `--no_vo` option, turn `.vo` file saving into a plugin.
#650
ejgallego
closed
6 months ago
0
[compat] Drop support for Coq 8.16, update README
#649
ejgallego
closed
7 months ago
0
LSP plugin mangling VSCode/ium Settings file
#648
jp-diegidio
opened
7 months ago
2
[vendor] Bump Coq and Coq SerAPI
#647
ejgallego
closed
7 months ago
0
[workspace] Be more resilient to CoqProject errors.
#646
ejgallego
closed
7 months ago
0
[code] Fix typo on package.json configuration section
#645
ejgallego
closed
7 months ago
0
[fleche] [doc] Interpret require via special custom path.
#644
ejgallego
closed
5 months ago
0
[memo] Add memo table for Require.
#643
ejgallego
closed
7 months ago
0
[coq] API to handle Require Ast specifically
#642
ejgallego
closed
7 months ago
0
[wip] File auto-build
#641
ejgallego
opened
7 months ago
1
[cleanup] Canonicalize request representation in theory
#640
ejgallego
closed
7 months ago
0
_CoqProject won't be loaded from subdirectory
#639
Alizter
opened
7 months ago
1
With Coq PR #18443, Prettyp.print_abbreviation takes an additional sigma
#638
herbelin
closed
7 months ago
1
[ci] [windows] Fix Dune 3.6.1 not available on setup-ocaml
#637
ejgallego
closed
7 months ago
0
[ci] Windows CI is broken due to outdated Dune version.
#636
ejgallego
closed
7 months ago
1
[vendor] Bump Coq
#635
ejgallego
closed
8 months ago
0
Better copying support
#634
Alizter
opened
8 months ago
1
Erroneous Coq files with incorrect AST ranges for valid steps
#633
pcarrott
closed
5 months ago
5
Ltac, Notation and Tactic Notation doesn't appear in the document overview
#632
Alizter
opened
8 months ago
1
[vendor] Bump Coq
#631
ejgallego
closed
8 months ago
0
[test suite] Check files from upstream on CI
#630
ejgallego
opened
8 months ago
1
[fleche] Experimental option for "lazy" document checking.
#629
ejgallego
closed
9 months ago
0
[meta] CoqPilot support issue
#628
ejgallego
opened
9 months ago
0
[requests] Allow not to postpone full document requests
#627
ejgallego
closed
9 months ago
0
[example] Example how to use the LSP client
#626
ejgallego
opened
9 months ago
0
[code] Don't trigger goals buffer action in general Markdown documents
#625
ejgallego
closed
9 months ago
0
[flèche] Store ranges in protocol-native encoding
#624
ineol
closed
3 months ago
1
Use ppx_inline_test for unit tests
#623
ineol
closed
9 months ago
8
[vendor] Bump Coq
#622
ejgallego
closed
9 months ago
0
[lsp] Requests input positions are not translated uniformly, and often handled as UTF-8 codepoints instead of UTF-16
#621
ejgallego
closed
3 months ago
11
Diagnostics report positions in UTF-8 code points
#620
ejgallego
closed
3 months ago
0
[plugin] Goal dump plugin.
#619
ejgallego
closed
5 months ago
2
[internal] Make diagnostic / messages severity types abstract
#618
ejgallego
closed
9 months ago
0
Coq-lsp doesn't work when filename includes a dash
#617
amblafont
opened
9 months ago
4
[error recovery] Recognize `Defined` and `Admitted` in lex recovery
#616
ejgallego
closed
9 months ago
0
[config] set `goal_after_tactic` default to `true`
#615
ejgallego
closed
9 months ago
0
Previous
Next