Bump Iris, fix FIXME.

opam.pins

-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 55294a275cc03823d941c678d236e36e00b785a5
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 7127e55309477c4a1db2cd43d58f65efa3431171

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. }