diff --git a/opam.pins b/opam.pins
index d2fdcfbfbff8504ea1b82dc8e39b532b4786cfa3..982bbc18bce9c4cf14f5bd677c314bc216436a72 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 73140880af6b19204077569b6c8d37504dc8814a..2c3f212c77f3dc437c727ec15f0291f987f840a4 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. }