Place the interpret-proof lens at the annotation top #83

Merged

marfavi merged 2 commits from fix/code-lens-annotation-top into main 2026-10-29 13:46:15 +01:00

Conversation 1 Commits 2 Files changed 2 +8 -9

marfavi commented 2026-10-28 14:50:49 +01:00

Owner

• Copy link
• Copy Markdown

Fixes #75

The lens now sits on the annotation, not on its PROOF clause.

Fixes #75 The lens now sits on the annotation, not on its PROOF clause.

marfavi added 1 commit 2026-10-28 14:50:49 +01:00

Place the interpret-proof lens at the annotation top (#75) db8569a1ed

michael approved these changes 2026-10-29 10:38:39 +01:00

marfavi added 1 commit 2026-10-29 13:42:16 +01:00

Merge remote-tracking branch 'origin/main' into fix/code-lens-annotation-top ... ff0b1d378c

# Conflicts:
#	examples/sumarray/sumarray.c

marfavi merged commit 8ea5858670 into main 2026-10-29 13:46:15 +01:00

Sign in to join this conversation.

Reviewers

No reviewers

michael

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

Assignees

Clear assignees

No assignees

2 participants

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!83

No description provided.