From 8ce92349df0d6bed5343c3f166152e12819f1d8a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 7 May 2022 16:24:26 +0200
Subject: [PATCH] fix accidental use of coPset domain
---
iris/algebra/dyn_reservation_map.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/iris/algebra/dyn_reservation_map.v b/iris/algebra/dyn_reservation_map.v
index f11f6b6b3..51d5affda 100644
--- a/iris/algebra/dyn_reservation_map.v
+++ b/iris/algebra/dyn_reservation_map.v
@@ -294,7 +294,7 @@ Section cmra.
- eapply set_infinite_subseteq, HE2inf. set_solver.
- intros i. rewrite left_id_L. destruct (Hdisj i) as [?|Hi]; first by left.
destruct (mf !! i) as [p|] eqn:Hp; last by left.
- apply (elem_of_dom_2 (D:=coPset)) in Hp. right. set_solver.
+ apply (elem_of_dom_2 (D:=gset _)), elem_of_gset_to_coPset in Hp. right. set_solver.
Qed.
Lemma dyn_reservation_map_reserve' :
ε ~~>: (λ x, ∃ E, set_infinite E ∧ x = dyn_reservation_map_token E).
--
GitLab