diff --git a/opam.pins b/opam.pins
index 132b6b01d40992f4f3d0d1b86bac07739286b9dd..3a65a2b9f02a5da100e02382a092f3b15ae8d623 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 5241c33d3013b81bb620b3cfd3cba1f2efdc5b2b
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq e0789039ed0dcb01b6249fec2d5a36f66e5de21c
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index c3e1b0c4fc9e88f408f80a6ae7bf4a2006c33394..1944f785c8df44dd2bfdcd25db962f11a333904c 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -54,8 +54,7 @@ Section sum.
     iSplit; iIntros "H".
     - iDestruct "H" as (vl) "[Hmt Hown]". iDestruct "Hown" as (i vl' vl'') "(% & % & Hown)".
       subst. iExists i. iDestruct (heap_mapsto_vec_cons with "Hmt") as "[$ Hmt]".
-      (* TODO: I should not have to say '[#]' here, similar to iDestruct ... as %.... *)
-      iAssert (⌜length vl' = (nth i tyl ∅).(ty_size)⌝%I) with "[#]" as %Hvl'.
+      iAssert (⌜length vl' = (nth i tyl ∅).(ty_size)⌝%I) as %Hvl'.
       { iApply ty_size_eq. done. }
       iDestruct (heap_mapsto_vec_app with "Hmt") as "[Hmt Htail]". iSplitL "Htail".
       + iExists vl''. rewrite (shift_loc_assoc_nat _ 1) Hvl'. iFrame. iPureIntro.
@@ -63,8 +62,7 @@ Section sum.
       + iExists vl'. by iFrame.
     - iDestruct "H" as (i) "[[Hmt1 Htail] Hown]".
       iDestruct "Hown" as (vl') "[Hmt2 Hown]". iDestruct "Htail" as (vl'') "[Hmt3 %]".
-      (* TODO: I should not have to say '[#]' here, similar to iDestruct ... as %.... *)
-      iAssert (⌜length vl' = (nth i tyl ∅).(ty_size)⌝%I) with "[#]" as %Hvl'.
+      iAssert (⌜length vl' = (nth i tyl ∅).(ty_size)⌝%I) as %Hvl'.
       { iApply ty_size_eq. done. } iExists (#i::vl'++vl'').
       rewrite heap_mapsto_vec_cons heap_mapsto_vec_app (shift_loc_assoc_nat _ 1) Hvl'.
       iFrame. iExists i, vl', vl''. iSplit; first done. iFrame. iPureIntro.
@@ -91,9 +89,8 @@ Section sum.
     intros tyl E κ l tid. iIntros (??) "#LFT Hown Htok". rewrite split_sum_mt.
     iMod (bor_exists with "LFT Hown") as (i) "Hown". set_solver.
     iMod (bor_sep with "LFT Hown") as "[Hmt Hown]". solve_ndisj.
-    (* FIXME: Why can't I directly frame Htok in the destruct after the following mod? *)
-    iMod ((nth i tyl ∅).(ty_share) with "LFT Hown Htok") as "[#Hshr Htok]"; try done.
-    iFrame "Htok". iMod (bor_fracture with "LFT [Hmt]") as "H'";[set_solver| |]; last eauto.
+    iMod ((nth i tyl ∅).(ty_share) with "LFT Hown Htok") as "[#Hshr $]"; try done.
+    iMod (bor_fracture with "LFT [Hmt]") as "H'";[set_solver| |]; last eauto.
       by iFrame.
   Qed.
   Next Obligation.