Add instance CMRADiscrete dec_agreeR.

8bfa7c46 · Robbert Krebbers · 15be3526 · 8bfa7c46
Commit 8bfa7c46 authored Feb 22, 2017 by Robbert Krebbers
--- 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.