diff --git a/opam.pins b/opam.pins
index 629a8a4ae63f1acd7aee4b9b87bd6774d0adf807..a96d0bbbc241d9a581b41a5ddefbe7f9139a57a7 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 039f9fd5f753337034dcbfbbdb311cebdfa93acf
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq c798ff4f78cd663c2a710b0af4e7af063b35580a
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index de2276bc2a116ff5680316adcbf04cefda43e657..c4f15b94f3754fbd71992e7018a1d0a1f0d957ad 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -342,7 +342,7 @@ Section lft_contexts.
     iMod (HE1 with "HE1 HL1") as (qE1) "[HE1 Hclose1]". done.
     iMod (HE2 with "HE2 HL2") as (qE2) "[HE2 Hclose2]". done.
     destruct (Qp_lower_bound qE1 qE2) as (q & qE1' & qE2' & -> & ->). iExists q.
-    rewrite !fractional (fractional_half_equiv qE) /elctx_interp big_sepL_app.
+    rewrite !fractional [elctx_interp E qE]fractional_half /elctx_interp big_sepL_app.
     iDestruct "HE1" as "[$ HE1]". iDestruct "HE2" as "[$ HE2]". iIntros "!> [Hq1 Hq2]".
     iMod ("Hclose1" with "[$HE1 $Hq1]") as "[$ $]". iApply "Hclose2". iFrame.
   Qed.