Skip to content
Snippets Groups Projects
Commit 455be639 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Update Iris.

parent 0df052f9
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
opam.pins
+ 1
− 1
View file @ 455be639
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq ea7913081b7554d4d8191c0cfe99bfd736d22343 coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 3d6525a57844edcc8868ec9271a0966bcc2a5e89
theories/typing/lib/rc.v
+ 1
− 2
View file @ 455be639
...@@ -163,8 +163,7 @@ Section code. ...@@ -163,8 +163,7 @@ Section code.
{ iExists None. auto. } { iExists None. auto. }
iSpecialize ("Hνend" with "[Hν1 Hν2]"). iSpecialize ("Hνend" with "[Hν1 Hν2]").
{ rewrite -H0. iFrame. } { rewrite -H0. iFrame. }
iApply wp_mask_mono; last iApply (wp_step_fupd with "Hνend"); [done..|try solve_ndisj|]. iApply wp_mask_mono; last iApply (wp_step_fupd with "Hνend"); [done..|solve_ndisj|].
{ (* FIXME: solve_ndisj should solve this... *) set_solver+. }
wp_read. iIntros "#Hν". iMod ("Hν†" with "Hν") as "Hown". iModIntro. wp_read. iIntros "#Hν". iMod ("Hν†" with "Hν") as "Hown". iModIntro.
iApply "HΦ". iFrame. iLeft. auto with iFrame. iApply "HΦ". iFrame. iLeft. auto with iFrame.
+ destruct Hst as [[??%leibniz_equiv]|[[q'' Hqa%leibniz_equiv] ?%pos_included]%prod_included]. + destruct Hst as [[??%leibniz_equiv]|[[q'' Hqa%leibniz_equiv] ?%pos_included]%prod_included].
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment