listen to rename of .v files and update annotationStore & crocq annotations #43

New issue

Open

opened 2026-10-15 15:02:50 +02:00 by EatOreo · 0 comments

EatOreo commented 2026-10-15 15:02:50 +02:00

Owner

• Copy link

No description provided.

marfavi added this to the Release roadmap project 2026-10-22 14:51:14 +02:00

marfavi added the

quick-pick

label 2026-10-28 14:23:25 +01:00

marfavi referenced this issue from a commit 2026-10-28 15:07:12 +01:00

Refresh annotations after files are renamed (#43)

marfavi referenced this issue from a pull request that will close it, 2026-10-28 15:07:15 +01:00

Update annotation links on rename #89

marfavi changed title from listen to rename of .v files and update annotationStore to listen to rename of .v files and update annotationStore & crocq annotations 2026-10-29 19:09:38 +01:00

marfavi referenced this issue from a commit 2026-10-29 19:55:55 +01:00

Refresh annotations after files are renamed (#43)

Sign in to join this conversation.

No Branch/Tag specified

Branches Tags

main

release/0.1.0

fix/resync-on-v-rename

feat/infer-inline-declare

feat/grammar-highlighting

feat/clightgen-command-in-status

fix/code-lens-annotation-top

feature/proof-status

fix/inline-clauses-review-findings

v0.1.0

Labels

Clear labels   

blocked

should wait for another issue to be addressed

  

bug

  

priority!

  

quick-pick

No labels

blocked

bug

priority!

quick-pick

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Release roadmap

Assignees

Clear assignees

No assignees

1 participant

Notifications

Subscribe

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set

Reference

code2rocq/crocq#43

No description provided.