From 9aeb8f2b89a708a6517bbc399876cff136190a41 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 12 Feb 2017 13:26:45 +0100
Subject: [PATCH] Bump Iris and remove a FIXME.

---
 opam.pins                  | 2 +-
 theories/lang/new_delete.v | 4 +---
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/opam.pins b/opam.pins
index 2e1903eb..221e0a3f 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 9ea6fa453f1b9ef1cd4b5b8a167d1fab717c895e
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq f1b30a2eb12d38bffd8a0aa541c90e3675af2a29
diff --git a/theories/lang/new_delete.v b/theories/lang/new_delete.v
index 1e7a42ba..b27b5d5f 100644
--- a/theories/lang/new_delete.v
+++ b/theories/lang/new_delete.v
@@ -25,9 +25,7 @@ Section specs.
     iIntros (? Φ) "HΦ". wp_lam. wp_op; intros ?.
     - wp_if. assert (n = 0) as -> by lia. iApply ("HΦ" $! _ []).
       rewrite heap_mapsto_vec_nil. auto.
-    - wp_if. wp_alloc l vl as "H↦" "H†".
-      (* FIXME: I have to state the coercion vec_to_list explicitly here. *)
-      iApply ("HΦ" $! _ (vec_to_list vl)).
+    - wp_if. wp_alloc l vl as "H↦" "H†". iApply ("HΦ" $! _ vl).
       rewrite vec_to_list_length -{2}Hsz Z2Nat.id //. iFrame. auto.
   Qed.
 
-- 
GitLab