turns out naming the module dec_agree_deprecated is not necessary

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.

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.