diff --git a/CHANGELOG.md b/CHANGELOG.md
index 44da725e29f4ab2144eadc61a7d730fcd225101f..fcf3fe79a1ec3519a288c2db638d26c283b7371b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,9 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 
 ## Iris 3.0 (unfinished)
 
+* There now is a deprecation process.  The modules `*.deprecated`
+  contains deprecated notations and definitions that are provided for
+  backwards compatibility and will be removed in a future version of Iris.
 * View shifts are radically simplified to just internalize frame-preserving
   updates.  Weakestpre is defined inside the logic, and invariants and view
   shifts with masks are also coded up inside Iris.  Adequacy of weakestpre
@@ -12,8 +15,9 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * Use OFEs instead of COFEs everywhere.  COFEs are only used for solving the
   recursive domain equation.  As a consequence, CMRAs no longer need a proof
   of completeness.
+  (The old `cofeT` is provided by `algebra.deprecated`.)
 * Renaming and moving things around: uPred and the rest of the base logic are
-  in [base_logic], while [program_logic] is for everything involving the
+  in `base_logic`, while `program_logic` is for everything involving the
   general Iris notion of a language.
 * With invariants and the physical state being handled in the logic, there
   is no longer any reason to demand the CMRA unit to be discrete.
diff --git a/_CoqProject b/_CoqProject
index aa3e00b81e811bf823fef7bae6bad36e54d5c3a9..419e8982165db35e68851f2430f61ca38b03f356 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -58,6 +58,7 @@ algebra/updates.v
 algebra/local_updates.v
 algebra/gset.v
 algebra/coPset.v
+algebra/deprecated.v
 base_logic/upred.v
 base_logic/primitive.v
 base_logic/derived.v