Fix compilation with latest Iris.

opam.pins

-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 939b747baa303ca3e2e1538cfd76fccd900596cf
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 2550dff5c235a7367390a26c0db9871adb8fe0e7

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' //.

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'.