Show Rocq diagnostics in contract comment blocks; add vars keyword and qualify variables when generating proof skeleton; generate proof skeleton automatically if exists #31

Merged

marfavi merged 7 commits from vars into main 2026-03-27 11:29:40 +01:00

Conversation 0 Commits 7 Files changed 15 +2284 -28

marfavi commented 2026-03-27 11:26:00 +01:00

Owner

• Copy link

No description provided.

marfavi added 6 commits 2026-03-27 11:26:00 +01:00

add vars keyword in contract comment b1615d01f1

generate proof skeleton d4bfc4ba4c

do work 9643a1af02

add some todos a01ce50185

auto expand variable with st from now on 0468960224

show Rocq diagnostics in contract comment blocks f7e790f6d9

marfavi added 1 commit 2026-03-27 11:27:57 +01:00

update diagram fb3dd10d2a

marfavi force-pushed vars from fb3dd10d2a to 072ba6dc16 2026-03-27 11:28:54 +01:00 Compare

marfavi merged commit b890c47feb into main 2026-03-27 11:29:40 +01:00

marfavi deleted branch vars 2026-03-27 11:29:41 +01:00

marfavi referenced this pull request from a commit 2026-03-27 11:29:41 +01:00

Show Rocq diagnostics in contract comment blocks; add vars keyword and qualify variables when generating proof skeleton; generate proof skeleton automatically if exists (#31)

Commenting is not possible because the repository is archived.

Reviewers

No reviewers

Labels

Clear labels

No items

No labels

Milestone

Clear milestone

No items

No milestone

Projects

Clear projects

No items

No project

Assignees

Clear assignees

No assignees

1 participant

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/imp2rocq!31

No description provided.