diff --git a/theories/atomic_sync.v b/theories/atomic_sync.v
index b716ddebe3c656b362e35279b1bbe8f99c1fdb6a..89b31d099b580681daca0ff1c2851be7308066f5 100644
--- a/theories/atomic_sync.v
+++ b/theories/atomic_sync.v
@@ -2,12 +2,10 @@
 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 deprecated frac.
+From iris.algebra Require Import agree 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 *)
+Definition syncR := prodR fracR (agreeR valC). (* track the local knowledge of ghost state *)
 Class syncG Σ := sync_tokG :> inG Σ syncR.
 Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)].
 
@@ -15,11 +13,13 @@ Instance subG_syncΣ {Σ} : subG syncΣ Σ → syncG Σ.
 Proof. by intros ?%subG_inG. Qed.
 
 Section atomic_sync.
-  Context `{EqDecision A, !heapG Σ, !lockG Σ, !inG Σ (prodR fracR (dec_agreeR A))}.
+  Context `{EqDecision A, !heapG Σ, !lockG Σ}.
+  Canonical AC := leibnizC A.
+  Context `{!inG Σ (prodR fracR (agreeR AC))}.
 
   (* TODO: Rename and make opaque; the fact that this is a half should not be visible
            to the user. *)
-  Definition gHalf (γ: gname) g : iProp Σ := own γ ((1/2)%Qp, DecAgree g).
+  Definition gHalf (γ: gname) g : iProp Σ := own γ ((1/2)%Qp, to_agree g).
 
   Definition atomic_seq_spec (ϕ: A → iProp Σ) α β (f x: val) :=
     (∀ g, {{ ϕ g ∗ α g }} f x {{ v, ∃ g', ϕ g' ∗ β g g' v }})%I.
@@ -49,8 +49,8 @@ Section atomic_sync.
       mk_syncer_spec mk_syncer → atomic_syncer_spec mk_syncer.
   Proof.
     iIntros (Hsync g0 Ï• ret) "HÏ• Hret".
-    iMod (own_alloc (((1 / 2)%Qp, DecAgree g0) ⋅ ((1 / 2)%Qp, DecAgree g0))) as (γ) "[Hg1 Hg2]".
-    { by rewrite pair_op dec_agree_idemp. }
+    iMod (own_alloc (((1 / 2)%Qp, to_agree g0) ⋅ ((1 / 2)%Qp, to_agree g0))) as (γ) "[Hg1 Hg2]".
+    { by rewrite pair_op agree_idemp. }
     iApply (Hsync (∃ g: A, ϕ g ∗ gHalf γ g)%I with "[Hg1 Hϕ]")=>//.
     { iExists g0. by iFrame. }
     iNext. iIntros (s) "#Hsyncer". iApply "Hret".
@@ -76,10 +76,10 @@ Section atomic_sync.
       iSpecialize ("Hvs2" $! v).
       iDestruct (m_frag_agree' with "[Hg'' Hg1]") as "[Hg %]"; first iFrame. subst.
       rewrite Qp_div_2.
-      iAssert (|==> own γ (((1 / 2)%Qp, DecAgree g') ⋅ ((1 / 2)%Qp, DecAgree g')))%I
+      iAssert (|==> own γ (((1 / 2)%Qp, to_agree g') ⋅ ((1 / 2)%Qp, to_agree g')))%I
               with "[Hg]" as ">[Hg1 Hg2]".
       { iApply own_update; last by iAssumption.
-        apply cmra_update_exclusive. by rewrite pair_op dec_agree_idemp. }
+        apply cmra_update_exclusive. by rewrite pair_op agree_idemp. }
       iMod ("Hvs2" with "[Hg1 Hβ]").
       { iExists g'. iFrame. }
       iModIntro. iSplitL "Hg2 HÏ•'"; last done.
diff --git a/theories/flat.v b/theories/flat.v
index c5aa9c3e2796b2e443037d038a7c3d46a15c675b..195a3ff6deaa8dc2bfba3683a9fa4976f43978ee 100644
--- a/theories/flat.v
+++ b/theories/flat.v
@@ -4,12 +4,10 @@ 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 deprecated gset gmap.
+From iris.algebra Require Import auth frac agree excl agree 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
@@ -49,7 +47,7 @@ Definition mk_flat : val :=
       let: "r" := loop "p" "s" "lk" in
       "r".
 
-Definition reqR := prodR fracR (dec_agreeR val). (* request x should be kept same *)
+Definition reqR := prodR fracR (agreeR valC). (* request x should be kept same *)
 Definition toks : Type := gname * gname * gname * gname * gname. (* a bunch of tokens to do state transition *)
 Definition tokmR : ucmraT := evmapR loc toks unitR. (* tie each slot to tokens *)
 Class flatG Σ := FlatG {
@@ -76,17 +74,17 @@ Section proof.
   Definition installed_s R (ts: toks) (f x: val) :=
     let '(γx, γ1, _, γ4, γq) := ts in
     (∃ (P: val → iProp Σ) Q,
-       own γx ((1/2)%Qp, DecAgree x) ∗ P x ∗ ({{ R ∗ P x }} f x {{ v, R ∗ Q x v }}) ∗
+       own γx ((1/2)%Qp, to_agree x) ∗ P x ∗ ({{ R ∗ P x }} f x {{ v, R ∗ Q x v }}) ∗
        saved_prop_own γq (Q x) ∗ own γ1 (Excl ()) ∗ own γ4 (Excl ()))%I.
 
   Definition received_s (ts: toks) (x: val) γr :=
     let '(γx, _, _, γ4, _) := ts in
-    (own γx ((1/2/2)%Qp, DecAgree x) ∗ own γr (Excl ()) ∗ own γ4 (Excl ()))%I.
+    (own γx ((1/2/2)%Qp, to_agree x) ∗ own γr (Excl ()) ∗ own γ4 (Excl ()))%I.
 
   Definition finished_s (ts: toks) (x y: val) :=
     let '(γx, γ1, _, γ4, γq) := ts in
     (∃ Q: val → val → iProp Σ,
-       own γx ((1/2)%Qp, DecAgree x) ∗ saved_prop_own γq (Q x) ∗
+       own γx ((1/2)%Qp, to_agree x) ∗ saved_prop_own γq (Q x) ∗
        Q x y ∗ own γ1 (Excl ()) ∗ own γ4 (Excl ()))%I.
 
   Definition evm := ev loc toks.
@@ -131,7 +129,7 @@ Section proof.
 
   Definition installed_recp (ts: toks) (x: val) (Q: val → iProp Σ) :=
     let '(γx, _, γ3, _, γq) := ts in
-    (own γ3 (Excl ()) ∗ own γx ((1/2)%Qp, DecAgree x) ∗ saved_prop_own γq Q)%I.
+    (own γ3 (Excl ()) ∗ own γx ((1/2)%Qp, to_agree x) ∗ saved_prop_own γq Q)%I.
 
   Lemma install_spec
         R P Q
@@ -148,7 +146,7 @@ Section proof.
     iMod (own_alloc (Excl ())) as (γ1) "Ho1"; first done.
     iMod (own_alloc (Excl ())) as (γ3) "Ho3"; first done.
     iMod (own_alloc (Excl ())) as (γ4) "Ho4"; first done.
-    iMod (own_alloc (1%Qp, DecAgree x)) as (γx) "Hx"; first done.
+    iMod (own_alloc (1%Qp, to_agree x)) as (γx) "Hx"; first done.
     iMod (saved_prop_alloc (F:=(ofe_funCF val idCF)) Q) as (γq) "#?".
     iInv N as "[Hrs >Hm]" "Hclose".
     iDestruct "Hm" as (m) "[Hm HRm]".
@@ -209,8 +207,8 @@ Section proof.
       + iDestruct "Hp" as (f' x') "(Hp & Hs)".
         wp_load. destruct ts as [[[[γx γ1] γ3] γ4] γq].
         iDestruct "Hs" as (P Q) "(Hx & Hpx & Hf' & HoQ & Ho1 & Ho4)".
-        iAssert (|==> own γx (((1/2/2)%Qp, DecAgree x') ⋅
-                               ((1/2/2)%Qp, DecAgree x')))%I with "[Hx]" as ">[Hx1 Hx2]".
+        iAssert (|==> own γx (((1/2/2)%Qp, to_agree x') ⋅
+                               ((1/2/2)%Qp, to_agree x')))%I with "[Hx]" as ">[Hx1 Hx2]".
         { iDestruct (own_update with "Hx") as "?"; last by iAssumption.
           rewrite -{1}(Qp_div_2 (1/2)%Qp).
           by apply pair_l_frac_op'. }
@@ -294,7 +292,7 @@ Section proof.
   Definition own_γ3 (ts: toks) := let '(_, _, γ3, _, _) := ts in own γ3 (Excl ()).
   Definition finished_recp (ts: toks) (x y: val) :=
     let '(γx, _, _, _, γq) := ts in
-    (∃ Q, own γx ((1 / 2)%Qp, DecAgree x) ∗ saved_prop_own γq (Q x) ∗ Q x y)%I.
+    (∃ Q, own γx ((1 / 2)%Qp, to_agree x) ∗ saved_prop_own γq (Q x) ∗ Q x y)%I.
 
   Lemma try_srv_spec R (s: loc) (lk: val) (γs γr γm γlk: gname) Φ :
     inv N (srv_stack_inv R γs γm γr s ∗ srv_tokm_inv γm) ∗
@@ -419,7 +417,8 @@ Section proof.
       iSpecialize ("Heq" $! a0). by iRewrite "Heq" in "HQ'".
     - iExFalso. iCombine "Hx" "Hx'" as "Hx".
       iDestruct (own_valid with "Hx") as %[_ H1].
-      rewrite pair_op //= dec_agree_ne in H1=>//.
+      rewrite pair_op //=  in H1=>//. apply to_agree_comp_valid in H1.
+      fold_leibniz. done.
   Qed.
 
 End proof.
diff --git a/theories/misc.v b/theories/misc.v
index bc4be1c2a278a69d445c0be05a677461de087eb2..89557c41b5c134a674bccf30cdad03337869fc87 100644
--- a/theories/misc.v
+++ b/theories/misc.v
@@ -2,20 +2,20 @@
 
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang proofmode notation.
-From iris.algebra Require Import auth frac gmap deprecated.
+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 dec_agree.
+Import uPred.
 
 Section lemmas.
   Lemma pair_l_frac_op' (p q: Qp) (g g': val):
-     ((p + q)%Qp, DecAgree g') ~~> (((p, DecAgree g') â‹… (q, DecAgree g'))).
-  Proof. by rewrite pair_op dec_agree_idemp frac_op'. Qed.
+     ((p + q)%Qp, to_agree g') ~~> (((p, to_agree g') â‹… (q, to_agree g'))).
+  Proof. by rewrite pair_op agree_idemp frac_op'. Qed.
 
   Lemma pair_l_frac_op_1' (g g': val):
-     (1%Qp, DecAgree g') ~~> (((1/2)%Qp, DecAgree g') â‹… ((1/2)%Qp, DecAgree g')).
-  Proof. by rewrite pair_op dec_agree_idemp frac_op' Qp_div_2. Qed.
+     (1%Qp, to_agree g') ~~> (((1/2)%Qp, to_agree g') â‹… ((1/2)%Qp, to_agree g')).
+  Proof. by rewrite pair_op agree_idemp frac_op' Qp_div_2. Qed.
   
 End lemmas.
 
@@ -60,26 +60,27 @@ Section big_op_later.
 End big_op_later.
 
 Section pair.
-  Context `{EqDecision A, !inG Σ (prodR fracR (dec_agreeR A))}.
+  Context {A : ofeT} `{EqDecision A, !Discrete A, !LeibnizEquiv A, !inG Σ (prodR fracR (agreeR A))}.
 
   Lemma m_frag_agree γm (q1 q2: Qp) (a1 a2: A):
-    own γm (q1, DecAgree a1) ∗ own γm (q2, DecAgree a2) ⊢ ⌜a1 = a2⌝.
+    own γm (q1, to_agree a1) ∗ own γm (q2, to_agree a2) ⊢ ⌜a1 = a2⌝.
   Proof.
     iIntros "[Ho Ho']".
     destruct (decide (a1 = a2)) as [->|Hneq]=>//.
     iCombine "Ho" "Ho'" as "Ho".
     iDestruct (own_valid with "Ho") as %Hvalid.
     exfalso. destruct Hvalid as [_ Hvalid].
-    simpl in Hvalid. apply dec_agree_op_inv in Hvalid. inversion Hvalid. subst. auto.
+    simpl in Hvalid. apply agree_op_inv in Hvalid. apply (inj to_agree) in Hvalid.
+    apply Hneq. by fold_leibniz.
   Qed.
   
   Lemma m_frag_agree' γm (q1 q2: Qp) (a1 a2: A):
-    own γm (q1, DecAgree a1) ∗ own γm (q2, DecAgree a2)
-    ⊢ own γm ((q1 + q2)%Qp, DecAgree a1) ∗ ⌜a1 = a2⌝.
+    own γm (q1, to_agree a1) ∗ own γm (q2, to_agree a2)
+    ⊢ own γm ((q1 + q2)%Qp, to_agree a1) ∗ ⌜a1 = a2⌝.
   Proof.
     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' dec_agree_idemp. by iFrame.
+    rewrite pair_op frac_op' agree_idemp. by iFrame.
   Qed.
 End pair.
diff --git a/theories/peritem.v b/theories/peritem.v
index c0143bb509844d830e2346523a3bc80efa1d3f24..47abaac21b17ab569d194a3856b53cd39320a5dd 100644
--- a/theories/peritem.v
+++ b/theories/peritem.v
@@ -1,12 +1,10 @@
 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 deprecated csum.
+From iris.algebra Require Import frac auth gmap 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/treiber.v b/theories/treiber.v
index c1db56b1f5872ba7454b3186e81cb86dd788edce..86608d4fbdf0d68abbd1d9168bc5340403d90c95 100644
--- a/theories/treiber.v
+++ b/theories/treiber.v
@@ -1,12 +1,10 @@
 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 deprecated csum.
+From iris.algebra Require Import frac auth gmap 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 :=