diff --git a/opam.pins b/opam.pins
index fd3eb4bef05e35eed4018fb61685bd07489e7ea1..396d7477d30b35af2e6dc00259a2c5c318a5e878 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 0cc2c6e098bfb05c056783b9212c9218fa46aa5e
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq b212b3faddae4b089f30ef1c7a27d43ebd3a1675
diff --git a/theories/atomic_incr.v b/theories/atomic_incr.v
index 65628b7bb4adba9dffde1c27978fb4fbf768079c..e7fa0c9385ab00afeb8675f50aa277fb0752c6dc 100644
--- a/theories/atomic_incr.v
+++ b/theories/atomic_incr.v
@@ -66,7 +66,7 @@ Section user.
   Lemma incr_2_safe:
     ∀ (x: Z), (WP incr_2 #x {{ _, True }})%I.
   Proof.
-    iIntros (x) "". (* FIXME: I did iIntros, this should not be needed. *)
+    iIntros (x).
     rewrite /incr_2 /=.
     wp_lam.
     wp_alloc l as "Hl".
diff --git a/theories/atomic_pcas.v b/theories/atomic_pcas.v
index 63358e33e6d5924c72e9cf615c70eb6241021c8f..103a57dbed32eda5a867c22b36f04377e481b25c 100644
--- a/theories/atomic_pcas.v
+++ b/theories/atomic_pcas.v
@@ -1,13 +1,13 @@
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
-From iris.algebra Require Import dec_agree frac.
+From iris.algebra Require Import agree frac.
 From iris_atomic Require Import sync atomic_sync.
 Import uPred.
 
 Section atomic_pair.
   Context `{!heapG Σ, !lockG Σ, !syncG Σ,
-            !inG Σ (prodR fracR (dec_agreeR (val * val)))} (N : namespace).
+            !inG Σ (prodR fracR (agreeR (prodC valC valC)))} (N : namespace).
   
   Definition pcas_seq : val :=
     λ: "ls" "ab",
diff --git a/theories/atomic_sync.v b/theories/atomic_sync.v
index 7c2906c6b86e9f13308fb5dbfb05b92ed5d1a68c..b716ddebe3c656b362e35279b1bbe8f99c1fdb6a 100644
--- a/theories/atomic_sync.v
+++ b/theories/atomic_sync.v
@@ -2,9 +2,11 @@
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
-From iris.algebra Require Import dec_agree frac.
+From iris.algebra Require Import deprecated frac.
 From iris_atomic Require Import atomic sync misc.
 
+Import dec_agree.
+
 Definition syncR := prodR fracR (dec_agreeR val). (* track the local knowledge of ghost state *)
 Class syncG Σ := sync_tokG :> inG Σ syncR.
 Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)].
diff --git a/theories/evmap.v b/theories/evmap.v
index 6dabdd893ef3b01cbef09a5e2fb984b7625b5032..48a65f136fffa338aedc651bbee56772e476af0f 100644
--- a/theories/evmap.v
+++ b/theories/evmap.v
@@ -1,9 +1,12 @@
 (* evmap.v -- generalized heap-like monoid composite *)
 From iris.base_logic Require Export invariants.
 From iris.program_logic Require Export weakestpre.
-From iris.algebra Require Export auth frac gmap dec_agree.
+From iris.algebra Require Export auth frac gmap.
+From iris.algebra Require deprecated.
 From iris.proofmode Require Import tactics.
 
+Export deprecated.dec_agree.
+
 Section evmap.
   Context (K A: Type) (Q: cmraT) `{Countable K, EqDecision A}.
   Definition evkR := prodR Q (dec_agreeR A).
diff --git a/theories/flat.v b/theories/flat.v
index 39b437064c4c0fb077c58bd6381aab4f98dc36a1..c5aa9c3e2796b2e443037d038a7c3d46a15c675b 100644
--- a/theories/flat.v
+++ b/theories/flat.v
@@ -4,10 +4,12 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
-From iris.algebra Require Import auth frac agree excl dec_agree gset gmap.
+From iris.algebra Require Import auth frac agree excl deprecated gset gmap.
 From iris.base_logic Require Import big_op saved_prop.
 From iris_atomic Require Import misc peritem sync evmap.
 
+Import dec_agree.
+
 Definition doOp : val :=
   λ: "p",
      match: !"p" with
diff --git a/theories/misc.v b/theories/misc.v
index 7d1b32660a56b575576c57340cd909b7a7bb6d9e..bc4be1c2a278a69d445c0be05a677461de087eb2 100644
--- a/theories/misc.v
+++ b/theories/misc.v
@@ -2,10 +2,11 @@
 
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang proofmode notation.
-From iris.algebra Require Import auth frac gmap dec_agree.
+From iris.algebra Require Import auth frac gmap deprecated.
 From iris.prelude Require Import countable.
 From iris.base_logic Require Import big_op auth fractional.
-Import uPred.
+
+Import uPred dec_agree.
 
 Section lemmas.
   Lemma pair_l_frac_op' (p q: Qp) (g g': val):
diff --git a/theories/peritem.v b/theories/peritem.v
index a506380c8baffeeb7792e4eb8be84f2b11c8c129..c0143bb509844d830e2346523a3bc80efa1d3f24 100644
--- a/theories/peritem.v
+++ b/theories/peritem.v
@@ -1,10 +1,12 @@
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import frac auth gmap dec_agree csum.
+From iris.algebra Require Import frac auth gmap deprecated csum.
 From iris.base_logic Require Import big_op.
 From iris_atomic Require Export treiber misc evmap.
 
+Import dec_agree.
+
 Section defs.
   Context `{heapG Σ, !evidenceG loc val unitR Σ} (N: namespace).
   Context (R: val → iProp Σ) `{∀ x, TimelessP (R x)}.
diff --git a/theories/simple_sync.v b/theories/simple_sync.v
index 50b11a931b5b7b4e465ce5934b741b63f4fc1cca..c15ce1ec68797a70526cafb32c6f9aa52a5ddf48 100644
--- a/theories/simple_sync.v
+++ b/theories/simple_sync.v
@@ -3,7 +3,7 @@
 From iris.program_logic Require Export weakestpre hoare.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris.heap_lang.lib Require Import spin_lock.
-From iris.algebra Require Import dec_agree frac.
+From iris.algebra Require Import frac.
 From iris_atomic Require Import sync.
 Import uPred.
 
diff --git a/theories/treiber.v b/theories/treiber.v
index 817c085963925704f320618d783a3961fab47c49..c1db56b1f5872ba7454b3186e81cb86dd788edce 100644
--- a/theories/treiber.v
+++ b/theories/treiber.v
@@ -1,10 +1,12 @@
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import frac auth gmap dec_agree csum.
+From iris.algebra Require Import frac auth gmap deprecated csum.
 From iris.base_logic Require Import big_op.
 From iris_atomic Require Import atomic misc.
 
+Import dec_agree.
+
 Definition new_stack: val := λ: <>, ref (ref NONE).
 
 Definition push: val :=