From c99ab2e5f8e75749b6c32ff94b1e52e767758b4c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 19 Sep 2016 13:43:53 +0200
Subject: [PATCH] Also change the core of coPset to be the identity.

---
 algebra/coPset.v | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/algebra/coPset.v b/algebra/coPset.v
index cc3aa38d2..f90ff8e5a 100644
--- a/algebra/coPset.v
+++ b/algebra/coPset.v
@@ -12,11 +12,11 @@ Section coPset.
 
   Instance coPset_valid : Valid coPset := λ _, True.
   Instance coPset_op : Op coPset := union.
-  Instance coPset_pcore : PCore coPset := λ _, Some ∅.
+  Instance coPset_pcore : PCore coPset := Some.
 
   Lemma coPset_op_union X Y : X ⋅ Y = X ∪ Y.
   Proof. done. Qed.
-  Lemma coPset_core_empty X : core X = ∅.
+  Lemma coPset_core_self X : core X = X.
   Proof. done. Qed.
   Lemma coPset_included X Y : X ≼ Y ↔ X ⊆ Y.
   Proof.
@@ -33,8 +33,7 @@ Section coPset.
     - solve_proper.
     - intros X1 X2 X3. by rewrite !coPset_op_union assoc_L.
     - intros X1 X2. by rewrite !coPset_op_union comm_L.
-    - intros X. by rewrite coPset_op_union coPset_core_empty left_id_L.
-    - intros X1 X2 _. by rewrite coPset_included !coPset_core_empty.
+    - intros X. by rewrite coPset_core_self idemp_L.
   Qed.
   Canonical Structure coPsetR := discreteR coPset coPset_ra_mixin.
 
-- 
GitLab