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

"Rocq model is stale" diagnostic should only apply if there are any crocq annotations in the C file #95

New issue
Open
opened 2026-10-30 10:34:30 +01:00 by EatOreo · 0 comments
EatOreo commented 2026-10-30 10:34:30 +01:00
Owner

If a C file does not have Crocq annotations we should ignore at and let users code their C without our diagnostics and code lenses

If a C file does not have Crocq annotations we should ignore at and let users code their C without our diagnostics and code lenses
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#95
No description provided.