diff --git a/opam.pins b/opam.pins
index 982bbc18bce9c4cf14f5bd677c314bc216436a72..614a4d53734f6fc4e73c02b9f25866876302f125 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 7127e55309477c4a1db2cd43d58f65efa3431171
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 646bfc85e7ea6313e62feecf4ebcbcd76a186e71
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 29f20d78a1a4a7eb0fa16fe5b8f8fa300e25ef03..403ddcffdab8e1c7311c961e0f6d745deb6d7bf1 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -274,7 +274,7 @@ Section typing.
       { iApply (bor_fracture with "LFT"); first done. by rewrite Qp_mult_1_r. }
       iApply ("Hf" with "LFT [] Htl [Htk] [Hk HκsI HL]").
       + iApply "HE'". iIntros "{$# Hf Hinh HE' LFT HE %}".
-        iInduction κs as [|κ κs] "IH" forall "Hκs"=> //=. iSplitL.
+        iInduction κs as [|κ κs] "IH"=> //=. iSplitL.
         { iApply lft_incl_trans; first done. iApply lft_intersect_incl_l. }
         iApply "IH". iAlways. iApply lft_incl_trans; first done. iApply lft_intersect_incl_r.
       + iSplitL; last done. iExists ϝ. iSplit; first by rewrite /= left_id.