diff --git a/theories/algebra/deprecated.v b/theories/algebra/deprecated.v
index 3ff595195b3de5228a84d27217d1ae5ea511d319..8a64ae6f854ce5386b31469224f5a6c706806e66 100644
--- a/theories/algebra/deprecated.v
+++ b/theories/algebra/deprecated.v
@@ -50,6 +50,8 @@ 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_total : CMRATotal dec_agreeR.
 Proof. intros x. by exists x. Qed.