From f82111d28ec58a6785e882831e727e9689a6cc67 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 26 Feb 2016 16:19:52 +0100
Subject: [PATCH] Make discrete_cmra_discrete global.
---
algebra/cmra.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/algebra/cmra.v b/algebra/cmra.v
index f2f0da685..2d55bbf36 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -516,7 +516,7 @@ Section discrete.
apply (timeless _), dist_le with n; auto with lia.
Qed.
Definition discreteRA : cmraT := CMRAT (cofe_mixin A) discrete_cmra_mixin.
- Instance discrete_cmra_discrete : CMRADiscrete discreteRA.
+ Global Instance discrete_cmra_discrete : CMRADiscrete discreteRA.
Proof. split. change (Discrete A); apply _. by intros x ?. Qed.
End discrete.
--
GitLab