diff --git a/opam.pins b/opam.pins
index d2fdcfbfbff8504ea1b82dc8e39b532b4786cfa3..982bbc18bce9c4cf14f5bd677c314bc216436a72 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 55294a275cc03823d941c678d236e36e00b785a5
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 7127e55309477c4a1db2cd43d58f65efa3431171
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index f0bcd83173baa9706a06b00b26b729f54112321f..1dbd8ee6e64cac86914d30947093d9475bc8a10f 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -165,16 +165,20 @@ Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
 
 Definition subst' (mx : binder) (es : expr) : expr → expr :=
   match mx with BNamed x => subst x es | BAnon => id end.
+
 Fixpoint subst_l (xl : list binder) (esl : list expr) (e : expr) : option expr :=
   match xl, esl with
   | [], [] => Some e
   | x::xl, es::esl => subst' x es <$> subst_l xl esl e
   | _, _ => None
   end.
+Arguments subst_l _%RustB _ _%E.
 
 Definition subst_v (xl : list binder) (vsl : vec val (length xl))
                    (e : expr) : expr :=
   Vector.fold_right2 (λ b, subst' b ∘ of_val) e _ (list_to_vec xl) vsl.
+Arguments subst_v _%RustB _ _%E.
+
 Lemma subst_v_eq (xl : list binder) (vsl : vec val (length xl)) e :
   Some $ subst_v xl vsl e = subst_l xl (of_val <$> vec_to_list vsl) e.
 Proof.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 55183c084441e6af707216957917af0489a3b39e..4071d4c64c60de00115d8df6a5e7010570fd25f1 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -76,7 +76,8 @@ Section fn.
     intros tid vl. unfold typed_body.
     do 12 f_equiv. f_contractive. do 16 ((eapply fp_E_proper; try reflexivity) || exact: Hfp || f_equiv).
     - rewrite !cctx_interp_singleton /=. do 5 f_equiv.
-      rewrite !tctx_interp_singleton /tctx_elt_interp /=. repeat (apply Hfp || f_equiv).
+      rewrite !tctx_interp_singleton /tctx_elt_interp /=.
+      do 5 f_equiv. apply type_dist2_dist. apply Hfp.
     - rewrite /tctx_interp !big_sepL_zip_with /=. do 4 f_equiv.
       cut (∀ n tid p i, Proper (dist n ==> dist n)
         (λ (l : list _), ∀ ty, ⌜l !! i = Some ty⌝ → tctx_elt_interp tid (p ◁ ty))%I).
diff --git a/theories/typing/lib/mutex/mutex.v b/theories/typing/lib/mutex/mutex.v
index 73140880af6b19204077569b6c8d37504dc8814a..8d86ce50f63ea0b8689595c98bfcf8fe5980bd0e 100644
--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -166,11 +166,8 @@ 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 (_ :: vl). rewrite heap_mapsto_vec_cons. iFrame.
-        (* FIXME: Why does calling `iFrame` twice even make a difference? *)
-        iFrame. eauto. }
+      - iExists _. iFrame. by rewrite uninit_own vec_to_list_length.
+      - iExists (#false :: vl). rewrite heap_mapsto_vec_cons. iFrame; eauto. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index e6591e2bd27bde54d844493c1f062ae4fd79e002..cb61f148920c86ef4fea3128bb0e2c891d6ed4d7 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -590,8 +590,8 @@ Section code.
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); #lr ◁ box (rc ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame "Hx". iFrame "Hr†". iExists [_].
-      rewrite heap_mapsto_vec_singleton /=. eauto 10 with iFrame. }
+      unlock. iFrame "Hx". iFrame "Hr†". iExists [# #l'].
+      rewrite heap_mapsto_vec_singleton /=. simpl. eauto 10 with iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 90b45aec53bb2b13d94d5efe1a0ef33a5f06ed56..456d4a80cafc08efd632f5527d20fcdcfdb0e114 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -279,7 +279,7 @@ Section code.
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} rc ty); #lr ◁ box (weak ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame "Hx". iFrame "Hr†". iExists [_].
+      unlock. iFrame "Hx". iFrame "Hr†". iExists [# #l'].
       rewrite heap_mapsto_vec_singleton /=. eauto 10 with iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
@@ -352,7 +352,7 @@ Section code.
     iApply (type_type _ _ _ [ x ◁ box (&shr{α} weak ty); #lr ◁ box (weak ty)]
         with "[] LFT HE Hna HL Hk [-]"); last first.
     { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val tctx_hasty_val' //.
-      unlock. iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton /=.
+      unlock. iFrame. iExists [# #l']. rewrite heap_mapsto_vec_singleton /=.
       auto 10 with iFrame. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index a7b8630ed089d617243c536d50ade4d91555d8b4..7267fbf52e63801c2a7c32238c1faf87c8973b70 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -137,7 +137,7 @@ Section rwlockreadguard_functions.
       iApply (type_type _ _ _ [ x ◁ box (uninit 1); #lx' ◁ rwlockreadguard α ty]
               with "[] LFT HE Hna HL Hk"); first last.
       { rewrite tctx_interp_cons tctx_interp_singleton tctx_hasty_val
-                tctx_hasty_val' //=. auto 10 with iFrame. }
+                tctx_hasty_val' //=; simpl. auto 10 with iFrame. }
       iApply type_jump; solve_typing.
   Qed.
 End rwlockreadguard_functions.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 9b2a19aebea0f470b0b56b88a8acd1f59d60f6e2..aa4fc4149d7af8e3fd8c586eb6721f54ce66d689 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -51,7 +51,7 @@ Instance: Params (@ty_size) 2.
 Instance: Params (@ty_own) 2.
 Instance: Params (@ty_shr) 2.
 
-Arguments ty_own {_ _} _ _ !_ /.
+Arguments ty_own {_ _} _ _ !_ / : simpl nomatch.
 
 Class TyWf `{typeG Σ} (ty : type) := { ty_lfts : list lft; ty_wf_E : elctx }.
 Arguments ty_lfts {_ _} _ {_}.
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 33dbb662b9cca63f308f2d9172fe8178464be112..dfa4a4385c64a0525797b506339fa9f0ec443cc1 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -31,15 +31,15 @@ Section case.
     edestruct @Forall2_lookup_l as (e & He & Hety); eauto.
     wp_read. iApply wp_case; [lia|by rewrite Nat2Z.id|]. iNext.
     destruct Hety as [Hety|Hety]; iApply (Hety with "LFT HE Hna HL HC");
-      rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //; iFrame "HT".
-    - iDestruct (ty.(ty_size_eq) with "Hown") as %<-.
+      rewrite !tctx_interp_cons !tctx_hasty_val' /= ?Hv //=; iFrame "HT".
+    - rewrite /own_ptr /=. iDestruct (ty.(ty_size_eq) with "Hown") as %<-.
       iSplitL "H↦i Hfi"; last iSplitR "H↦vl'' Hfvl''".
       + rewrite shift_loc_0. iFrame. iExists [ #i]. rewrite heap_mapsto_vec_singleton.
         iFrame. iExists [_], []. auto.
-      + iFrame. iExists _. iFrame.
+      + eauto with iFrame.
       + rewrite -EQlen app_length minus_plus -(shift_loc_assoc_nat _ 1).
         iFrame. iExists _. iFrame. rewrite uninit_own. auto.
-    - rewrite -EQlen app_length -(Nat.add_1_l (_+_)) -!freeable_sz_split. iFrame.
+    - rewrite /= -EQlen app_length -(Nat.add_1_l (_+_)) -!freeable_sz_split. iFrame.
       iExists (#i :: vl' ++ vl''). iNext. rewrite heap_mapsto_vec_cons heap_mapsto_vec_app.
       iFrame. iExists i, vl', vl''. rewrite /= -EQlen app_length nth_lookup EQty /=. auto.
   Qed.