diff --git a/opam.pins b/opam.pins
index ccdcb41f37f1ca81dee3afb7556afd9b52f92a56..e603372b8bc78e49c519409eda35d9bbaa6c6fa8 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 939b747baa303ca3e2e1538cfd76fccd900596cf
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 2550dff5c235a7367390a26c0db9871adb8fe0e7
diff --git a/theories/typing/type_sum.v b/theories/typing/type_sum.v
index 3df1f459d0d6dfc65aab2cbe83b5930aa66ee1d2..a529af731d6af0554b1f7726a55f5b94f6ce70bc 100644
--- a/theories/typing/type_sum.v
+++ b/theories/typing/type_sum.v
@@ -233,7 +233,7 @@ Section case.
     rewrite -(take_drop (ty.(ty_size)) vl1) heap_mapsto_vec_app.
     iDestruct "H↦vl1" as "[H↦vl1 H↦pad]".
     iDestruct (ty_size_eq with "Hty") as "#>%".
-    iApply wp_fupd. iApply (wp_memcpy with "[$H↦vl1 $H↦2]"); [|lia|].
+    iApply (wp_memcpy with "[$H↦vl1 $H↦2]"); [|lia|].
     { rewrite take_length. lia. }
     iNext; iIntros "[H↦vl1 H↦2]".
     rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val' //.
diff --git a/theories/typing/unsafe/refcell/ref_code.v b/theories/typing/unsafe/refcell/ref_code.v
index 97284a3bf8256a1b3bc3aff03aa8caf8718a38a0..a87066598b55179481720fce4ec32f90d3dba9a1 100644
--- a/theories/typing/unsafe/refcell/ref_code.v
+++ b/theories/typing/unsafe/refcell/ref_code.v
@@ -52,7 +52,7 @@ Section ref_functions.
         revert Heq. intros [= <-]. destruct st'' as [[ag q'] n].
         revert Hle=>/Some_included_2 /Some_pair_included
                [/Some_pair_included_total_1 [/agree_included Heq _] _] [[Hag _] _].
-        iExists q', n. iPureIntro. repeat constructor. apply Cinlr_equiv.
+        iExists q', n. iPureIntro. repeat constructor. apply Cinr_equiv.
         do 2 constructor; last done. apply agree_op_inv. by rewrite comm -Heq. }
     iDestruct "Hst" as %[st' [-> Hst']]%equiv_Some_inv_r'.
     destruct st' as [|[[]]|]; try by inversion Hst'. apply (inj Cinr), (inj2 pair) in Hst'.