diff --git a/opam.pins b/opam.pins
index 7da437340d56f33ca433871148f3922f50a16182..2e1903ebaf7e28bffc3eaf1ef59bbbcc18f91257 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 8b9f59ab3630176149621661c8f3ee7b456dfe5f
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 9ea6fa453f1b9ef1cd4b5b8a167d1fab717c895e
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 9e0263e9bb5a15b0ab8d17de675e9a1521ca1077..887fbc2c1ba3d1f0685ee843d6b6d9e7756fa9d7 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -51,8 +51,7 @@ Proof.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
   iMod (heap_alloc with "Hσ") as "[Hσ Hl]"; [done..|].
   iModIntro; iSplit=> //. iFrame.
-  (* FIXME: Merging these two into one "iApply" doesn't work. *)
-  iSpecialize ("HΦ" $! _ (length init)). iApply ("HΦ" $! (list_to_vec init)).
+  iApply ("HΦ" $! _ _ (list_to_vec init)).
   rewrite vec_to_list_of_list. auto.
 Qed.
 
diff --git a/theories/lifetime/model/raw_reborrow.v b/theories/lifetime/model/raw_reborrow.v
index e563a17ee28a20300bba23705bb4d8eb789373ad..fadea3d20e6b368d8fdf776af22bd58109dc1f1d 100644
--- a/theories/lifetime/model/raw_reborrow.v
+++ b/theories/lifetime/model/raw_reborrow.v
@@ -40,8 +40,7 @@ Proof.
   iMod (slice_empty with "Hislice Hbox") as "[HP Hbox]"; first done.
   { by rewrite lookup_fmap HB. }
   iMod (own_bor_update_2 with "HB● Hi") as "[HB● Hi]".
-  { eapply auth_update. (* FIXME: eapply singleton_local_update loops. *)
-    apply: singleton_local_update; last eapply
+  { eapply auth_update, singleton_local_update; last eapply
      (exclusive_local_update _ (1%Qp, to_agree (Bor_rebor κ'))); last done.
     rewrite /to_borUR lookup_fmap. by rewrite HB. }
   iAssert (▷?q lft_inv A κ)%I with "[H◯ HB● HB Hvs' Hinh' Hbox]" as "Hκ".
diff --git a/theories/typing/own.v b/theories/typing/own.v
index af0840fcd55852f17ce5aa6ab87e4407df21bb61..94192e2ca3585666b2ef3ce4a89f552b47822d8e 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -155,8 +155,7 @@ Section own.
     iIntros (Hsync κ tid1 tid2 l) "H". iDestruct "H" as (l') "[Hm #Hshr]".
     iExists _. iFrame "Hm". iAlways. iIntros (F q) "% Htok".
     iMod ("Hshr" with "[] Htok") as "Hfin"; first done. iModIntro. iNext.
-    iClear "Hshr". (* FIXME: Using "{HShr} [HShr $]" for the intro pattern in the following line doesn't work. *)
-    iMod "Hfin" as "[Hshr $]". by iApply Hsync.
+    iMod "Hfin" as "{Hshr} [Hshr $]". by iApply Hsync.
   Qed.
 End own.
 
@@ -225,9 +224,7 @@ Section typing.
     typed_body E L C T (let: x := new [ #n ] in e).
   Proof.
     intros ???? Htyp. eapply type_let. done. by apply type_new_instr. solve_typing.
-    iIntros (v). iApply typed_body_mono; [done| |done|].
-    (* FIXME : why can't we iApply Htyp? *)
-    2:by iDestruct (Htyp v) as "$".
+    iIntros (v). iApply typed_body_mono; [done| |done|by iApply (Htyp v)].
     by apply (tctx_incl_frame_r _ [_] [_]), subtype_tctx_incl, own_mono.
   Qed.
 
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 16be9ec89affe76c7cd7ba68af3e3821fa1265cc..d82cf7b1227025e3a569b52c6ecd6821c3646101 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -262,9 +262,8 @@ Section typing_rules.
   Proof.
     iIntros (Hsz Hwrt Hread) "!#". iIntros (tid qE) "#LFT Htl HE HL HT".
     iApply (type_memcpy_iris with "[] [] [$LFT $Htl $HE $HL HT]"); try done.
-    (* TODO: This is kind of silly, why can't I iApply the assumptions directly? *)
-    { iPoseProof Hwrt as "Hwrt". done. }
-    { iPoseProof Hread as "Hread". done. }
+    { iApply Hwrt. }
+    { iApply Hread. }
     { by rewrite tctx_interp_cons tctx_interp_singleton. }
     rewrite tctx_interp_cons tctx_interp_singleton. auto.
   Qed.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 77a4aa7eecb2fa79804383fcf4d8ceb82d694de0..dc0d11b991dcdd6f9289aae7033da0e3a439a3d3 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -155,11 +155,7 @@ Section type_context.
 
   Global Instance tctx_ty_copy T p ty :
     CopyC T → Copy ty → CopyC ((p ◁ ty) :: T).
-  Proof.
-    (* TODO RJ: Should we have instances that PersistentP respects equiv? *)
-    intros ???. rewrite /PersistentP tctx_interp_cons.
-    apply uPred.sep_persistent; by apply _.
-  Qed.
+  Proof. intros ???. rewrite tctx_interp_cons. apply _. Qed.
 
   (** Send typing contexts *)
   Class SendC (T : tctx) :=
diff --git a/theories/typing/unsafe/spawn.v b/theories/typing/unsafe/spawn.v
index aa79c626e971be535b336173b097980c1b8ba997..56a50af553e1a3ef256b59528dcf4dfd6437a529 100644
--- a/theories/typing/unsafe/spawn.v
+++ b/theories/typing/unsafe/spawn.v
@@ -23,14 +23,8 @@ Section join_handle.
          end%I;
        ty_shr κ tid l := True%I |}.
   Next Obligation. by iIntros (ty tid [|[[]|][]]) "H"; try iDestruct "H" as "[]". Qed.
-  Next Obligation.
-    (* FIXME: Replacing the % by a _ below fails. *)
-    iIntros "* % _ _ $". auto.
-  Qed.
-  Next Obligation.
-    (* FIXME: for some reason, `iIntros "*" does not do anything here. *)
-    iIntros (?) "* _ _ _". auto.
-  Qed.
+  Next Obligation. iIntros "* _ _ _ $". auto. Qed.
+  Next Obligation. iIntros (?) "**"; auto. Qed.
 
   Lemma join_handle_subtype ty1 ty2 :
     type_incl ty1 ty2 -∗ type_incl (join_handle ty1) (join_handle ty2).