From 094150fb6a7369d76870bd531034712b70b9dfa6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 16 Jan 2016 02:45:48 +0100
Subject: [PATCH] Declare COFE on state as a canonical structure.

---
 iris/parameter.v | 4 +++-
 iris/resources.v | 2 +-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/iris/parameter.v b/iris/parameter.v
index 9a70891f9..671bdbab7 100644
--- a/iris/parameter.v
+++ b/iris/parameter.v
@@ -22,4 +22,6 @@ Lemma icmra_map_ext (Σ : iParam) {A B} (f g : A -n> B) m :
   (∀ x, f x ≡ g x) → icmra_map Σ f m ≡ icmra_map Σ g m.
 Proof.
   by intros ?; apply equiv_dist=> n; apply icmra_map_ne=> ?; apply equiv_dist.
-Qed.
\ No newline at end of file
+Qed.
+
+Canonical Structure istateC Σ := leibnizC (istate Σ).
\ No newline at end of file
diff --git a/iris/resources.v b/iris/resources.v
index 42758006b..632a15d30 100644
--- a/iris/resources.v
+++ b/iris/resources.v
@@ -2,7 +2,7 @@ Require Export modures.fin_maps modures.agree modures.excl iris.parameter.
 
 Record res (Σ : iParam) (A : cofeT) := Res {
   wld : mapRA positive (agreeRA (laterC A));
-  pst : exclRA (leibnizC (istate Σ));
+  pst : exclRA (istateC Σ);
   gst : icmra Σ (laterC A);
 }.
 Add Printing Constructor res.
-- 
GitLab