Skip to content

GitLab

Commit 6396d121 authored by Ralf Jung's avatar Ralf Jung
Browse files

Fix flat.v which broke for some reason 

Also update IRIS_VERSION because I can't be bothered to downgrade now...
parent 129cd4e8
Show whitespace changes
Inline Side-by-side
IRIS_VERSION
View file @ 6396d121
bb5e21f21fd1b5be820005eb53750f84270ab4ec 05a588df59ddfdc2e7a4aec5a98a50614c819693
_CoqProject
View file @ 6396d121
-Q . iris_atomic -Q . iris_atomic
-Q iris iris
atomic.v atomic.v
sync.v sync.v
atomic_incr.v atomic_incr.v
......
flat.v
View file @ 6396d121
...@@ -305,9 +305,9 @@ Section proof. ...@@ -305,9 +305,9 @@ Section proof.
iIntros (?) "(#? & #? & #? & HΦ)". iIntros (?) "(#? & #? & #? & HΦ)".
wp_seq. wp_let. wp_seq. wp_let.
wp_bind (try_acquire _). iApply try_acquire_spec. wp_bind (try_acquire _). iApply try_acquire_spec.
iFrame "#". iSplit; last by wp_if. iFrame "#". iNext. iIntros ([]); last by (iIntros; wp_if).
(* acquired the lock *) (* acquired the lock *)
iIntros "Hlocked [Ho2 HR]". iIntros "[Hlocked [Ho2 HR]]".
wp_if. wp_bind (! _)%E. wp_if. wp_bind (! _)%E.
iInv N as "[H >Hm]" "Hclose". iInv N as "[H >Hm]" "Hclose".
iDestruct "H" as (xs' hd') "[>Hs [>Hxs HRs]]". iDestruct "H" as (xs' hd') "[>Hs [>Hxs HRs]]".
......
Markdown is supported
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