diff --git a/opam.pins b/opam.pins
index dbf958d081b063ab955462c8b3bb10b663a3c0e3..132b6b01d40992f4f3d0d1b86bac07739286b9dd 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq fb1712dd9da4d05ca2c919748633801934369d0d
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 5241c33d3013b81bb620b3cfd3cba1f2efdc5b2b
diff --git a/theories/typing/cont.v b/theories/typing/cont.v
index 22c26a3add6cda55620915dd72a7892826cf69e0..3fc7d459e43eab96694e5cd1eb1580cfc317547a 100644
--- a/theories/typing/cont.v
+++ b/theories/typing/cont.v
@@ -34,7 +34,6 @@ Section typing.
     iIntros (args) "Htl HL HT". iApply wp_rec; try done.
     { rewrite Forall_fmap Forall_forall=>? _. rewrite /= to_of_val. eauto. }
     { by rewrite -(subst_v_eq (_ :: _) (RecV _ _ _ ::: _)). }
-    (* FIXME: iNext here unfolds things in the context. *)
     iNext. iApply (Hecont with "* HEAP LFT Htl HE HL [HC] HT").
     by iApply "IH".
   Qed.