diff --git a/opam.pins b/opam.pins
index ac0de2142e79b964c31a9ec6b9bf98cd8662214d..9087d1ed13556140819293adf4d9c13459b4c69d 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 01d12014855abe6adaea20bbb35b1e9beadff14e
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 398bae9d092b6568cf8d504ca98d8810979eea33
diff --git a/theories/atomic.v b/theories/atomic.v
index 84ddd9a335cfb8c11191765a8b7e7a41c5b8e44a..e3343ef823e35897ac8c52f11efa07da57d003b7 100644
--- a/theories/atomic.v
+++ b/theories/atomic.v
@@ -2,7 +2,6 @@
 
 From iris.base_logic Require Export fancy_updates.
 From iris.program_logic Require Export hoare weakestpre.
-From iris.prelude Require Export coPset.
 Import uPred.
 
 Section atomic.
diff --git a/theories/atomic_incr.v b/theories/atomic_incr.v
index e7fa0c9385ab00afeb8675f50aa277fb0752c6dc..a7ac870640b39301448d290de5f8951fde7c0c86 100644
--- a/theories/atomic_incr.v
+++ b/theories/atomic_incr.v
@@ -2,7 +2,6 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris_atomic Require Import atomic.
 From iris.proofmode Require Import tactics.
-From iris.prelude Require Import coPset.
 From iris.heap_lang.lib Require Import par.
 
 Section incr.
diff --git a/theories/flat.v b/theories/flat.v
index 07b98eb41d634721be03e754687addacd90767aa..35ec113109d0244b517be3385f60ae814bb86b70 100644
--- a/theories/flat.v
+++ b/theories/flat.v
@@ -166,7 +166,7 @@ Section proof.
         subst. rewrite Qp_div_2. iMod ("Hclose" with "[-HR Hor HΦ]").
         { iNext. iDestruct "Hp" as "[Hp1 Hp2]". iRight. iRight.
           iRight. iExists x5, v. iFrame. iExists Q. iFrame. }
-        iApply "HΦ". iFrame.
+        iApply "HΦ". iFrame. done.
       * iDestruct "Hp" as (? ?) "[? Hs]". iDestruct "Hs" as (?) "(_ & _ & _ & >Ho1' & _)".
         iApply excl_falso. iFrame.
     - destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (? x) "(_ & _ & >Ho2' & _)".
@@ -207,7 +207,7 @@ Section proof.
       { iFrame. iFrame "#". }
       iNext. iIntros "HRf".
       wp_seq. wp_proj. iApply (IHxs with "[-HΦ]")=>//.
-      iFrame "#"; first by iFrame. eauto.
+      iFrame "#"; first by iFrame.
   Qed.
 
   Lemma try_srv_spec R (s: loc) (lk: val) (γr γm γlk: gname) Φ :
@@ -282,7 +282,7 @@ Section proof.
     iIntros (P Q x) "#Hf".
     iIntros "!# Hp". wp_let. wp_bind (install _ _ _).
     iApply (install_spec R P Q f x γm γr s with "[-]")=>//.
-    { iFrame. iFrame "#". eauto. }
+    { iFrame. iFrame "#". }
     iNext. iIntros (p [[[[γx γ1] γ3] γ4] γq]) "[(Ho3 & Hx & HoQ) #?]".
     wp_let. wp_bind (loop _ _ _).
     iApply (loop_spec with "[-Hx HoQ]")=>//.
@@ -290,13 +290,13 @@ Section proof.
     iNext. iIntros (? ?) "Hs".
     iDestruct "Hs" as (Q') "(Hx' & HoQ' & HQ')".
     destruct (decide (x = a)) as [->|Hneq].
-    - iDestruct (saved_prop_agree with "[HoQ HoQ']") as "Heq"; first by iFrame.
+    - iDestruct (saved_prop_agree with "[$HoQ] [HoQ']") as "Heq"; first by iFrame.
       wp_let. iDestruct (uPred.cofe_funC_equivI with "Heq") as "Heq".
-      iSpecialize ("Heq" $! a0). by iRewrite "Heq" in "HQ'".
+      iSpecialize ("Heq" $! a0). by iRewrite -"Heq" in "HQ'".
     - iExFalso. iCombine "Hx" "Hx'" as "Hx".
       iDestruct (own_valid with "Hx") as %[_ H1].
-      rewrite pair_op //=  in H1=>//. apply to_agree_comp_valid in H1.
-      fold_leibniz. done.
+      rewrite //= in H1.
+      by apply agree_op_inv' in H1.
   Qed.
 
 End proof.
diff --git a/theories/misc.v b/theories/misc.v
index 89557c41b5c134a674bccf30cdad03337869fc87..19269fd2246937a45ce072826358b44eff5f96f2 100644
--- a/theories/misc.v
+++ b/theories/misc.v
@@ -3,7 +3,6 @@
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris.algebra Require Import auth frac gmap agree.
-From iris.prelude Require Import countable.
 From iris.base_logic Require Import big_op auth fractional.
 
 Import uPred.
@@ -36,8 +35,9 @@ Section heap_extra.
     ~((q1 + q2)%Qp ≤ 1%Qp)%Qc →
     p ↦{q1} a ∗ p ↦{q2} b ⊢ False.
   Proof.
-    iIntros (?) "Hp". 
-    iDestruct (@mapsto_valid_2 with "Hp") as %H'. done.
+    iIntros (?) "Hp".
+    iDestruct "Hp" as "[Hl Hr]".
+    iDestruct (@mapsto_valid_2 with "Hl Hr") as %H'. done.
   Qed.
 
 End heap_extra.
@@ -81,6 +81,6 @@ Section pair.
     iIntros "[Ho Ho']".
     iDestruct (m_frag_agree with "[Ho Ho']") as %Heq; first iFrame.
     subst. iCombine "Ho" "Ho'" as "Ho".
-    rewrite pair_op frac_op' agree_idemp. by iFrame.
+    by iFrame.
   Qed.
 End pair.
diff --git a/theories/peritem.v b/theories/peritem.v
index 76a54ad56793035019ee3a43e718cea271954d04..156600d856b00bbfafb593eae56b172ef212bfa4 100644
--- a/theories/peritem.v
+++ b/theories/peritem.v
@@ -54,7 +54,7 @@ Section proofs.
     { iFrame. iExists [], l.
       iFrame. simpl. eauto. }
     iMod (inv_alloc N _ (∃ xs : list val, is_bag_R N R xs s)%I with "[-HΦ]") as "#?"; first eauto.
-    iApply "HΦ". iFrame "#".
+    iApply "HΦ". iFrame "#". done.
   Qed.
   
   Lemma push_spec (s: loc) (x: val):
diff --git a/theories/simple_sync.v b/theories/simple_sync.v
index c15ce1ec68797a70526cafb32c6f9aa52a5ddf48..a27fbc908f8ec5454e2daba80b015d3c559c7127 100644
--- a/theories/simple_sync.v
+++ b/theories/simple_sync.v
@@ -33,7 +33,7 @@ Section syncer.
     iSpecialize ("Hf" with "[R HP]"); first by iFrame.
     iApply wp_wand_r.  iSplitL "Hf"; first done.
     iIntros (v') "[HR HQv]". wp_let. wp_bind (release _).
-    iApply (release_spec with "[$HR $Hl $Hlocked]").
+    iApply (release_spec with "[$Hl $HR $Hlocked]").
     iNext. iIntros "_". by wp_seq.
   Qed.
 End syncer.
diff --git a/theories/treiber.v b/theories/treiber.v
index 86608d4fbdf0d68abbd1d9168bc5340403d90c95..40aa648741e6b19c208056dbbb4197b6bf48ee65 100644
--- a/theories/treiber.v
+++ b/theories/treiber.v
@@ -64,17 +64,17 @@ Section proof.
         simpl. iDestruct "Hys" as (hd' ?) "(Hhd & Hys')".
         iExFalso. iDestruct "Hxs" as (?) "Hhd'".
         (* FIXME: If I dont use the @ here and below through this file, it loops. *)
-        by iDestruct (@mapsto_agree with "[$Hhd $Hhd']") as %?.
+        by iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %?.
     - induction ys as [|y ys' IHys'].
       + iIntros (hd) "(Hxs & Hys)".
         simpl.
         iExFalso. iDestruct "Hxs" as (? ?) "(Hhd & _)".
         iDestruct "Hys" as (?) "Hhd'".
-        by iDestruct (@mapsto_agree with "[$Hhd $Hhd']") as %?.
+        by iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %?.
       + iIntros (hd) "(Hxs & Hys)".
         simpl. iDestruct "Hxs" as (? ?) "(Hhd & Hxs')".
         iDestruct "Hys" as (? ?) "(Hhd' & Hys')".
-        iDestruct (@mapsto_agree with "[$Hhd $Hhd']") as %[= Heq].
+        iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %[= Heq].
         subst. iDestruct (IHxs' with "[Hxs' Hys']") as "%"; first by iFrame.
         by subst.
   Qed.
@@ -173,9 +173,9 @@ Section proof.
         { iRight. iExists y', (q / 2 / 2)%Qp, hd', xs'.
           destruct xs as [|x' xs''].
           - simpl. iDestruct "Hhd''" as (?) "H".
-            iExFalso. by iDestruct (@mapsto_agree with "[$Hhd1 $H]") as %?.
+            iExFalso. by iDestruct (@mapsto_agree with "[$Hhd1] [$H]") as %?.
           - simpl. iDestruct "Hhd''" as (hd''' ?) "(Hhd'' & Hxs'')".
-            iDestruct (@mapsto_agree with "[$Hhd1 $Hhd'']") as %[=].
+            iDestruct (@mapsto_agree with "[$Hhd1] [$Hhd'']") as %[=].
             subst.
             iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst.
             repeat (iSplitR "Hxs1 Hs"; first done).