diff --git a/opam.pins b/opam.pins
index 2e1903ebaf7e28bffc3eaf1ef59bbbcc18f91257..221e0a3f085dfecaf02f97c9e4afadceb9f74c7e 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 1e7a42ba0ea3d4bb29ed6809f27739d0b49810f6..b27b5d5fdbc965c02ebff737a8a1c691612838d2 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.