From ae3de6b564f5429ae1dc59fb14cde446fa0e4161 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 9 May 2017 11:35:21 +0200
Subject: [PATCH] Bump Iris, fix FIXME.
---
opam.pins | 2 +-
theories/typing/lib/mutex/mutex.v | 3 +--
2 files changed, 2 insertions(+), 3 deletions(-)
diff --git a/opam.pins b/opam.pins
index d2fdcfbf..982bbc18 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 55294a275cc03823d941c678d236e36e00b785a5
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 7127e55309477c4a1db2cd43d58f65efa3431171
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 73140880..2c3f212c 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -166,8 +166,7 @@ Section code.
(* TODO: It would be nice to say [{#}] as the last spec pattern to clear the context in there. *)
{ rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val' // tctx_hasty_val' //.
iFrame. iSplitL "Hx".
- - iExists _. iFrame. rewrite uninit_own vec_to_list_length.
- by iNext. (* FIXME: Just "done" should work here. *)
+ - iExists _. iFrame. by rewrite uninit_own vec_to_list_length.
- iExists (_ :: vl). rewrite heap_mapsto_vec_cons. iFrame.
(* FIXME: Why does calling `iFrame` twice even make a difference? *)
iFrame. eauto. }
--
GitLab