F2 rename annotation links #97

New issue

Open

opened 2026-10-30 11:14:24 +01:00 by EatOreo · 0 comments

EatOreo commented 2026-10-30 11:14:24 +01:00

Owner

• Copy link
• Copy Markdown

if i F2 rename for instance s.v:renaming_this i would like that the name of the Rocq definition/Theorem is also updated

if i F2 rename for instance `s.v:renaming_this` i would like that the name of the Rocq definition/Theorem is also updated

EatOreo added this to the Release roadmap project 2026-10-30 13:57:55 +01:00

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#97

No description provided.