diff --git a/opam.pins b/opam.pins
index 642f2e56a3400e35bac618a9b5ed355c9fef0386..8868ac832f86730265e263d3f020bf51de135b91 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq b0418bd57b9341dbf5e58669c689201daa561bd7
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq b863cfd7640f5dccb14c17e9ffefb475f1b7d0d8
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index b5c53cd372102560077256c6852c4a0370004f16..f3f69a16ec4acd4a46b088adfc0446138b8e090f 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -1,5 +1,5 @@
 From Coq Require Import Min.
-From iris.prelude Require Import coPset.
+From stdpp Require Import coPset.
 From iris.algebra Require Import cmra_big_op gmap frac agree.
 From iris.algebra Require Import csum excl auth.
 From iris.base_logic Require Import big_op lib.fractional.
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index e770632fbf7d41725a99a49e31628cf26450cfb4..96df4989001e658b8b1338391126d58c3746768e 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -1,6 +1,6 @@
 From iris.program_logic Require Export language ectx_language ectxi_language.
-From iris.prelude Require Export strings.
-From iris.prelude Require Import gmap.
+From stdpp Require Export strings.
+From stdpp Require Import gmap.
 Set Default Proof Using "Type".
 
 Open Scope Z_scope.
diff --git a/theories/lang/races.v b/theories/lang/races.v
index 1ba1a13fa8399c8656945f0235f17e2b5b30d6aa..6cc6f95bddf46888244d815208fd880e2c9e425d 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -1,4 +1,4 @@
-From iris.prelude Require Import gmap.
+From stdpp Require Import gmap.
 From iris.program_logic Require Export hoare.
 From iris.program_logic Require Import adequacy.
 From lrust.lang Require Import tactics.
diff --git a/theories/lang/tactics.v b/theories/lang/tactics.v
index 99dc74648ca31bca924fd04e2d46dfb1beb3bafe..7ebfc8c5e1f8b48e8c9b3668f79e216f8e868400 100644
--- a/theories/lang/tactics.v
+++ b/theories/lang/tactics.v
@@ -1,4 +1,4 @@
-From iris.prelude Require Import fin_maps.
+From stdpp Require Import fin_maps.
 From lrust.lang Require Export lang.
 Set Default Proof Using "Type".
 
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index c6171e0bc002b1cc9a9da73bafb35c95dd552770..4684b65d115f0ae967368e629234dcd33e5d3632 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Import frac.
-From iris.prelude Require Export gmultiset strings.
+From stdpp Require Export gmultiset strings.
 From iris.base_logic.lib Require Export invariants.
 From iris.base_logic.lib Require Import boxes fractional.
 Set Default Proof Using "Type".
diff --git a/theories/typing/unsafe/refcell/ref_code.v b/theories/typing/unsafe/refcell/ref_code.v
index c373300da32e5cdf98f408aca4d3d10062461164..ac08fb9dadd677ec76c972688d96d7dd314ccb55 100644
--- a/theories/typing/unsafe/refcell/ref_code.v
+++ b/theories/typing/unsafe/refcell/ref_code.v
@@ -182,7 +182,7 @@ Section ref_functions.
       - destruct Heq as [?%leibniz_equiv ?%leibniz_equiv]. simpl in *. subst.
         iExists None. iFrame. iMod (own_update with "H●◯") as "$".
         { apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
-          apply op_local_update_cancellable_empty, _. }
+          apply cancel_local_update_empty, _. }
         iApply "H†". replace 1%Qp with (q'+q'')%Qp by naive_solver. iFrame.
       - destruct Hincl as [ [=] |[ (?&?&[=]&?) | (?&?&[=<-]&[=<-]&[[q0 n']EQ]) ]].
         destruct EQ as [?%leibniz_equiv ?%leibniz_equiv]. simpl in *. subst.
@@ -191,7 +191,7 @@ Section ref_functions.
         iExists (Some (_, Cinr (q0, n'))). iFrame. iMod (own_update with "H●◯") as "$".
         { apply auth_update_dealloc.
           rewrite -(agree_idemp (to_agree _)) -pair_op -Cinr_op -pair_op Some_op.
-          apply (op_local_update_cancellable_empty (reading_st q ν)), _. }
+          apply (cancel_local_update_empty (reading_st q ν)), _. }
         iExists ν. iFrame. iApply step_fupd_intro; first done. iIntros "!>".
         iSplitR; first done. iExists (q+q'')%Qp. iFrame.
         by rewrite assoc (comm _ q0 q). }
diff --git a/theories/typing/unsafe/refcell/refcell_code.v b/theories/typing/unsafe/refcell/refcell_code.v
index 396076aa1f2fdd951792dde4fda5694df4e885c3..fa185e27664170c2c25f383903b3be0cfba20f5e 100644
--- a/theories/typing/unsafe/refcell/refcell_code.v
+++ b/theories/typing/unsafe/refcell/refcell_code.v
@@ -184,7 +184,7 @@ Section refcell_functions.
           { apply auth_update_alloc,
             (op_local_update_discrete _ _ (reading_st (q'/2)%Qp ν))=>-[Hagv _].
             split; [|split].
-            - by rewrite -Hag /= agree_idemp.
+            - by rewrite /= -Hag agree_idemp.
             - change ((q'/2+q)%Qp ≤ 1%Qp)%Qc. rewrite -Hqq' comm -{2}(Qp_div_2 q').
               apply Qcplus_le_mono_l. rewrite -{1}(Qcplus_0_l (q'/2)%Qp).
               apply Qcplus_le_mono_r, Qp_ge_0.
diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/unsafe/refcell/refmut_code.v
index 8d29b53cd55a46ed6b5628dfaf585eeec5b05880..32ff0c6cd4eabc66876ceeaf8632b1bee6fc4952 100644
--- a/theories/typing/unsafe/refcell/refmut_code.v
+++ b/theories/typing/unsafe/refcell/refmut_code.v
@@ -147,7 +147,7 @@ Section refmut_functions.
     iMod ("Hcloseβ" with ">[H↦lrc H● H◯ Hb] Hna") as "[Hβ Hna]".
     { iExists None. iFrame. iMod (own_update_2 with "H● H◯") as "$"; last done.
       apply auth_update_dealloc. rewrite -(right_id None _ (Some _)).
-      apply op_local_update_cancellable_empty, _. }
+      apply cancel_local_update_empty, _. }
     iMod ("Hcloseα" with "Hβ") as "Hα". wp_seq.
     iAssert (elctx_interp [☀ α] qE) with "[Hα]" as "HE".
     { by rewrite /elctx_interp big_sepL_singleton. }