From bc1afae4becb539544a131f5eb4a051695455ae3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 6 May 2022 15:34:42 +0200
Subject: [PATCH] stop using coPset

---
 iris/algebra/dyn_reservation_map.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris/algebra/dyn_reservation_map.v b/iris/algebra/dyn_reservation_map.v
index 6570c8865..f11f6b6b3 100644
--- a/iris/algebra/dyn_reservation_map.v
+++ b/iris/algebra/dyn_reservation_map.v
@@ -282,10 +282,10 @@ Section cmra.
     intros [Hmap [Hinf Hdisj]].
     (* Pick a fresh set disjoint from the existing tokens [Ef] and map [mf],
        such that both that set [E1] and the remainder [E2] are infinite. *)
-    edestruct (coPset_split_infinite (⊤ ∖ (Ef ∪ dom coPset mf))) as
+    edestruct (coPset_split_infinite (⊤ ∖ (Ef ∪ (gset_to_coPset $ dom (gset _) mf)))) as
         (E1 & E2 & HEunion & HEdisj & HE1inf & HE2inf).
     { rewrite -difference_difference_L.
-        by apply difference_infinite, dom_finite. }
+      by apply difference_infinite, gset_to_coPset_finite. }
     exists (dyn_reservation_map_token E1).
     split; first by apply HQ. clear HQ.
     rewrite dyn_reservation_map_validN_eq /=.
-- 
GitLab