From e9c1712b8d0be1ca9ada9d41e6c069eb2b12a0ee Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 30 Jun 2016 01:16:28 +0200
Subject: [PATCH] Define discreteUR constructor.
---
algebra/cmra.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 3fa2eb417..21e945304 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -698,8 +698,8 @@ End discrete.
Notation discreteR A ra_mix :=
(CMRAT A discrete_cofe_mixin (discrete_cmra_mixin ra_mix)).
-Notation discreteLeibnizR A ra_mix :=
- (CMRAT A (@discrete_cofe_mixin _ equivL _) (discrete_cmra_mixin ra_mix)).
+Notation discreteUR A ra_mix ucmra_mix :=
+ (UCMRAT A discrete_cofe_mixin (discrete_cmra_mixin ra_mix) ucmra_mix).
Global Instance discrete_cmra_discrete `{Equiv A, PCore A, Op A, Valid A,
@Equivalence A (≡)} (ra_mix : RAMixin A) : CMRADiscrete (discreteR A ra_mix).
--
GitLab