From e7046bfb99cc44c1213e5eda9219af489048e328 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 7 Feb 2025 09:49:54 +0100
Subject: [PATCH] Forward compatibility for
 https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/555

---
 theories/lifetime/model/primitive.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 8801035c..5a6020ad 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -36,7 +36,7 @@ Lemma own_ilft_auth_agree (I : gmap lft lft_names) κ γs :
 Proof.
   iIntros "HI Hκ". iDestruct (own_valid_2 with "HI Hκ")
     as %[[? [Hl ?]]%singleton_included_l _]%auth_both_valid_discrete.
-  iPureIntro. apply elem_of_dom. unfold to_ilftUR in *. simplify_map_eq.
+  iPureIntro. apply elem_of_dom. rewrite /to_ilftUR lookup_fmap in Hl.
   destruct (fmap_Some_equiv_1 _ _ _ Hl) as (?&?&?). eauto.
 Qed.
 
-- 
GitLab