code2rocq/imp2rocq
Archived
Watch
3
0
Fork
You've already forked imp2rocq
 0
Code Issues 25 Pull requests Projects 2 Wiki Activity

hook ind i rocq/coq lsp #4

Open
opened 2026-02-26 10:45:46 +01:00 by EatOreo · 1 comment
EatOreo commented 2026-02-26 10:45:46 +01:00
Owner

vi skal nok kommunikere med rocqs language server om stuff. Evt bare se om model filen vi genererer er valid.

vi skal nok kommunikere med rocqs language server om stuff. Evt bare se om model filen vi genererer er valid.
EatOreo added this to the Kanban project 2026-02-26 10:45:46 +01:00
marfavi commented 2026-02-26 10:48:51 +01:00
Owner

step 1 er at finde ud af at checke om rocq langauge server er installeret, og ellers prompte til at downloade den extension

step 1 er at finde ud af at checke om rocq langauge server er installeret, og ellers prompte til at downloade den extension
EatOreo self-assigned this 2026-03-04 13:56:25 +01:00
Commenting is not possible because the repository is archived.
No Branch/Tag specified
Branches Tags
main
report
refactor-documents
parser
No results found.
Labels
Clear labels
No items
No labels
Milestone
Clear milestone
No items
No milestone
Projects
Clear projects
No items
No project
Kanban
Assignees
Clear assignees
No assignees
EatOreo
2 participants
Due date
The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Depends on
#18 Glue LS should do INCREMENTAL document sync
code2rocq/imp2rocq
Reference
code2rocq/imp2rocq#4
No description provided.