From 6396d121448735a43c08b05167daf9be3c2b029c Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 2 Nov 2016 14:05:26 +0100
Subject: [PATCH] Fix flat.v which broke for some reason

Also update IRIS_VERSION because I can't be bothered to downgrade now...
---
 IRIS_VERSION | 2 +-
 _CoqProject  | 1 -
 flat.v       | 4 ++--
 3 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/IRIS_VERSION b/IRIS_VERSION
index bd534da..608d866 100644
--- a/IRIS_VERSION
+++ b/IRIS_VERSION
@@ -1 +1 @@
-bb5e21f21fd1b5be820005eb53750f84270ab4ec
+05a588df59ddfdc2e7a4aec5a98a50614c819693
diff --git a/_CoqProject b/_CoqProject
index b0ab474..3d0e6a3 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,5 +1,4 @@
 -Q . iris_atomic
--Q iris iris
 atomic.v
 sync.v
 atomic_incr.v
diff --git a/flat.v b/flat.v
index 6fc1ee8..6f3d1d7 100644
--- a/flat.v
+++ b/flat.v
@@ -305,9 +305,9 @@ Section proof.
     iIntros (?) "(#? & #? & #? & HΦ)".
     wp_seq. wp_let.
     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 *)
-    iIntros "Hlocked [Ho2 HR]".
+    iIntros "[Hlocked [Ho2 HR]]".
     wp_if. wp_bind (! _)%E.
     iInv N as "[H >Hm]" "Hclose".
     iDestruct "H" as (xs' hd') "[>Hs [>Hxs HRs]]".
-- 
GitLab