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

we call vsRocqApi.getDocumentProofs() more than necessary #59

New issue
Open
opened 2026-10-21 10:35:53 +02:00 by EatOreo · 0 comments
EatOreo commented 2026-10-21 10:35:53 +02:00
Owner

pass the proofs to getProofBlock and getDefinitionRange instead of vsRocqApi: VsRocqApi, proofDocumentUri: vscode.Uri,

pass the proofs to getProofBlock and getDefinitionRange instead of vsRocqApi: VsRocqApi, proofDocumentUri: vscode.Uri,
marfavi changed title from we call vsRocqApi.getDocumentProofs() more than neccessary to we call vsRocqApi.getDocumentProofs() more than necessary 2026-10-22 14:47:34 +02: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
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#59
No description provided.