Skip to content
Snippets Groups Projects

Made refcell state coercion implementation agnostic

Merged Ike Mulder requested to merge snyke7/lambda-rust:ike/ucmra_fixes into master

This MR changes how some shorthand notation for the refcell state type was declared as a Coercion in Coq.
In particular, it makes the coercion work with iris!971, but it is also shorter and (in my opinion) more readable.

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
Please register or sign in to reply
Loading