diff --git a/opam.pins b/opam.pins
index bd50b2ef080c891df37847bfb9cdc36e26d750f3..b496f750fc3ef03c16bcba873827a7483400ccee 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 09d97eae9eba95ebf5539a0b32e88bfc0b61c0fe
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 02bc52b4d905eb635940ff8545d59676ad44ea8c
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 473df8bfb0fc0a1bf446c9539438149721c8990d..42a811c8841819345de222fcccb9cb08cdfa6b7d 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -229,7 +229,7 @@ Section typing.
   Proof.
     iIntros (<- tid eq) "#LFT $ $ $ Hp". rewrite tctx_interp_singleton.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
-    iDestruct "Hown" as "[H↦∗: >H†]". iDestruct "H↦∗:" as (vl) "[>H↦ Hown]".
+    iDestruct "Hown" as "[H↦: >H†]". iDestruct "H↦:" as (vl) "[>H↦ Hown]".
     rewrite tctx_interp_nil. iDestruct (ty_size_eq with "Hown") as "#>EQ".
     iDestruct "EQ" as %<-. iApply (wp_delete with "[-]"); auto; [].
     rewrite freeable_sz_full. by iFrame.