diff --git a/CHANGELOG.md b/CHANGELOG.md
index aa2753d8e770920fdfd5ab4660c6ae060e69b902..d7eb3f4682000330f12b210dff2f4f84ea922e44 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -18,7 +18,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   recursive domain equation.  As a consequence, CMRAs no longer need a proof of
   completeness.  (The old `cofeT` is provided by `algebra.deprecated`.)
 * Implement a new agreement construction.  Unlike the old one, this one
-  preserves discreteness.
+  preserves discreteness.  dec_agree is thus no longer needed and has been moved
+  to 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 general
   Iris notion of a language.
diff --git a/theories/algebra/deprecated.v b/theories/algebra/deprecated.v
index 753d956e785fe5f4eab82945a8622f4942a018a3..45024d71d45224bcb88f85f1861a5fcd54277f23 100644
--- a/theories/algebra/deprecated.v
+++ b/theories/algebra/deprecated.v
@@ -6,10 +6,7 @@ From iris.algebra Require Import ofe cmra.
 Notation cofeT := ofeT (only parsing).
 
 (* Deprecated 2016-12-09. Use agree instead. *)
-(* The module is called dec_agree_deprecated because if it was just dec_agree,
-   it would still be imported by "From iris Import dec_agree", and people would
-   not notice they use sth. deprecated. *)
-Module dec_agree_deprecated.
+Module dec_agree.
 Local Arguments validN _ _ _ !_ /.
 Local Arguments valid _ _  !_ /.
 Local Arguments op _ _ _ !_ /.
@@ -76,4 +73,4 @@ End dec_agree.
 
 Arguments dec_agreeC : clear implicits.
 Arguments dec_agreeR _ {_}.
-End dec_agree_deprecated.
+End dec_agree.