Open newly generated proof document so that navigation works instantly #92

New issue

Open

opened 2026-10-29 14:06:59 +01:00 by EatOreo · 0 comments

EatOreo commented 2026-10-29 14:06:59 +01:00

Owner

• Copy link
• Copy Markdown

after calling crocq.createProofFiles we can do vscode.workspace.openTextDocument on the created file

after calling crocq.createProofFiles we can do vscode.workspace.openTextDocument on the created file

marfavi added this to the Release roadmap project 2026-10-29 15:34:58 +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#92

No description provided.