From 69446a0ba3bdfe2d03923fe1f6d83c49baa2678d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 3 Sep 2024 11:18:18 +0200
Subject: [PATCH] Remove use of `map_Forall_insert_1`.
---
iris/algebra/lib/gmap_view.v | 10 ++++------
1 file changed, 4 insertions(+), 6 deletions(-)
diff --git a/iris/algebra/lib/gmap_view.v b/iris/algebra/lib/gmap_view.v
index c93ef00a2..390acb80b 100644
--- a/iris/algebra/lib/gmap_view.v
+++ b/iris/algebra/lib/gmap_view.v
@@ -398,13 +398,11 @@ Section lemmas.
intros ?? Hm'.
induction m' as [|k v m' ? IH] using map_ind; decompose_map_disjoint.
{ rewrite big_opM_empty left_id_L right_id. done. }
- rewrite IH //.
- 2:{ by eapply map_Forall_insert_1_2. }
- rewrite big_opM_insert // assoc.
+ apply map_Forall_insert in Hm' as [??]; last done.
+ rewrite IH //. rewrite big_opM_insert // assoc.
apply cmra_update_op; last done.
- rewrite -insert_union_l. apply (gmap_view_alloc _ k dq); [|done|].
- - by apply lookup_union_None.
- - eapply Hm'. erewrite lookup_insert. done.
+ rewrite -insert_union_l. apply (gmap_view_alloc _ k dq); [|done..].
+ by apply lookup_union_None.
Qed.
Lemma gmap_view_delete m k v :
--
GitLab