From 8bfa7c4671de9aeffb39489fdaa940962bd5e73e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 22 Feb 2017 18:34:37 +0100
Subject: [PATCH] Add instance CMRADiscrete dec_agreeR.

---
 theories/algebra/deprecated.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/algebra/deprecated.v b/theories/algebra/deprecated.v
index 3ff595195..8a64ae6f8 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.
 
-- 
GitLab