Skip to content

Made refcell state coercion implementation agnostic

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