code2rocq/crocq
code2rocq/crocq
Watch
3
2
Fork
You've already forked crocq
 0
Code Issues 18 Pull requests 3 Projects 1 Releases 1 Packages 2 Activity Actions

Warn when editing a spec/invariant in .v files where the .c file has defined it inline #94

New issue
Open
opened 2026-10-29 15:26:59 +01:00 by marfavi · 0 comments
marfavi commented 2026-10-29 15:26:59 +01:00
Owner

saving the .c file would overwrite the change when rebuilding the model

saving the .c file would overwrite the change when rebuilding the model
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
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#94
No description provided.