diff --git a/opam.pins b/opam.pins
index a1c04ed52b1e65e953dc09fda752e4b0cba049cd..4e9b917ac3b68c2a8195710288d0f2f2cefd6462 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq ea7913081b7554d4d8191c0cfe99bfd736d22343
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 3d6525a57844edcc8868ec9271a0966bcc2a5e89
diff --git a/theories/typing/lib/rc.v b/theories/typing/lib/rc.v
index 583aec81dea8f9e3802ca7c371e23fe19ae55259..b546de5bc4ee3e18ec16640b48070af23604fb76 100644
--- a/theories/typing/lib/rc.v
+++ b/theories/typing/lib/rc.v
@@ -163,8 +163,7 @@ Section code.
         { iExists None. auto. }
         iSpecialize ("Hνend" with "[Hν1 Hν2]").
         { rewrite -H0. iFrame. }
-        iApply wp_mask_mono; last iApply (wp_step_fupd with "Hνend"); [done..|try solve_ndisj|].
-        { (* FIXME: solve_ndisj should solve this... *) set_solver+. }
+        iApply wp_mask_mono; last iApply (wp_step_fupd with "Hνend"); [done..|solve_ndisj|].
         wp_read. iIntros "#Hν". iMod ("Hν†" with "Hν") as "Hown". iModIntro.
         iApply "HΦ". iFrame. iLeft. auto with iFrame.
       + destruct Hst as [[??%leibniz_equiv]|[[q'' Hqa%leibniz_equiv] ?%pos_included]%prod_included].