diff --git a/CHANGELOG.md b/CHANGELOG.md
index 76b0086d98a7403f626705839b52bf0eac3a5934..68ffabbab7dc6cc46439bd201f0c0af32913cfec 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -186,6 +186,8 @@ Coq 8.10, 8.11, and 8.12 are newly supported by this release, and Coq 8.7 and
   and can be installed with opam; see
   [iris/string-ident](https://gitlab.mpi-sws.org/iris/string-ident) for details.
 * Add `auto` hint for `∗-∗`.
+* Remove the long-deprecated `cofeT` alias (for `ofeT`) and `dec_agree` RA (use
+  `agree` instead).
 
 **Changes in `algebra`:**
 
diff --git a/_CoqProject b/_CoqProject
index 824d3c1f43ffd4e5960b7d9a40b767ea42883533..7e5bfbc2686f17443245972fdabce37a17677d77 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -33,7 +33,6 @@ theories/algebra/local_updates.v
 theories/algebra/gset.v
 theories/algebra/gmultiset.v
 theories/algebra/coPset.v
-theories/algebra/deprecated.v
 theories/algebra/proofmode_classes.v
 theories/algebra/ufrac.v
 theories/algebra/namespace_map.v
diff --git a/theories/algebra/deprecated.v b/theories/algebra/deprecated.v
deleted file mode 100644
index d91ece95affa891911e3ed583502710dbc9f953d..0000000000000000000000000000000000000000
--- a/theories/algebra/deprecated.v
+++ /dev/null
@@ -1,79 +0,0 @@
-From iris.algebra Require Import ofe cmra.
-Set Default Proof Using "Type".
-
-(* Old notation for backwards compatibility. *)
-
-(* Deprecated 2016-11-22. Use ofeT instead. *)
-Notation cofeT := ofeT (only parsing).
-
-(* Deprecated 2016-12-09. Use agree instead. *)
-Module dec_agree.
-Local Arguments validN _ _ _ !_ /.
-Local Arguments valid _ _  !_ /.
-Local Arguments op _ _ _ !_ /.
-Local Arguments pcore _ _ !_ /.
-
-(* This is isomorphic to option, but has a very different RA structure. *)
-Inductive dec_agree (A : Type) : Type :=
-  | DecAgree : A → dec_agree A
-  | DecAgreeBot : dec_agree A.
-Arguments DecAgree {_} _.
-Arguments DecAgreeBot {_}.
-Instance maybe_DecAgree {A} : Maybe (@DecAgree A) := λ x,
-  match x with DecAgree a => Some a | _ => None end.
-
-Section dec_agree.
-Context `{EqDecision A}.
-Implicit Types a b : A.
-Implicit Types x y : dec_agree A.
-
-Instance dec_agree_valid : Valid (dec_agree A) := λ x,
-  if x is DecAgree _ then True else False.
-Canonical Structure dec_agreeO : ofeT := leibnizO (dec_agree A).
-
-Instance dec_agree_op : Op (dec_agree A) := λ x y,
-  match x, y with
-  | DecAgree a, DecAgree b => if decide (a = b) then DecAgree a else DecAgreeBot
-  | _, _ => DecAgreeBot
-  end.
-Instance dec_agree_pcore : PCore (dec_agree A) := Some.
-
-Definition dec_agree_ra_mixin : RAMixin (dec_agree A).
-Proof.
-  apply ra_total_mixin; apply _ || eauto.
-  - intros [?|] [?|] [?|]; by repeat (simplify_eq/= || case_match).
-  - intros [?|] [?|]; by repeat (simplify_eq/= || case_match).
-  - intros [?|]; by repeat (simplify_eq/= || case_match).
-  - by intros [?|] [?|] ?.
-Qed.
-
-Canonical Structure dec_agreeR : cmraT :=
-  discreteR (dec_agree A) dec_agree_ra_mixin.
-
-Global Instance dec_agree_cmra_discrete : CmraDiscrete dec_agreeR.
-Proof. apply discrete_cmra_discrete. Qed.
-Global Instance dec_agree_cmra_total : CmraTotal dec_agreeR.
-Proof. intros x. by exists x. Qed.
-
-(* Some properties of this CMRA *)
-Global Instance dec_agree_core_id (x : dec_agreeR) : CoreId x.
-Proof. by constructor. Qed.
-
-Lemma dec_agree_ne a b : a ≠ b → DecAgree a ⋅ DecAgree b = DecAgreeBot.
-Proof. intros. by rewrite /= decide_False. Qed.
-
-Lemma dec_agree_idemp (x : dec_agree A) : x â‹… x = x.
-Proof. destruct x; by rewrite /= ?decide_True. Qed.
-
-Lemma dec_agree_op_inv (x1 x2 : dec_agree A) : ✓ (x1 ⋅ x2) → x1 = x2.
-Proof. destruct x1, x2; by repeat (simplify_eq/= || case_match). Qed.
-
-Lemma DecAgree_included a b : DecAgree a ≼ DecAgree b ↔ a = b.
-Proof.
-  split. intros [[c|] [=]%leibniz_equiv]. by simplify_option_eq. by intros ->.
-Qed.
-End dec_agree.
-
-Arguments dec_agreeO : clear implicits.
-Arguments dec_agreeR _ {_}.
-End dec_agree.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index bfee521735f2180482818458127a972e34e76bfc..52eb7fab840597485e6ad544a1c9d74ab8fd6434 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1368,6 +1368,7 @@ Tactic Notation "iModIntro" uconstr(sel) :=
 Tactic Notation "iModIntro" := iModIntro _.
 
 (** DEPRECATED *)
+#[deprecated(note = "Use iModIntro instead")]
 Tactic Notation "iAlways" := iModIntro.
 
 (** * Later *)