From c788b94ea0c8937ef50461837b23ea3ec73833c4 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@cnrs.fr>
Date: Mon, 31 Mar 2025 17:15:48 +0200
Subject: [PATCH] Thou shalt not use generated names.
---
theories/lifetime/model/accessors.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index acab5721..0404645e 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -167,7 +167,7 @@ Proof.
iMod ("Hclose'" with "[-Hbor Hclose]") as "_".
{ iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
iLeft. iFrame "%". iExists _, _. iFrame. }
- iExists κ''. iFrame "#". iIntros "!>* HvsQ HQ". clear -HE.
+ iExists κ''. iFrame "#". iIntros "!> %Q HvsQ HQ". clear -HE.
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
iDestruct (own_bor_auth with "HI Hbor") as %Hκ'.
rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
@@ -235,7 +235,7 @@ Proof.
as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
iMod (slice_delete_full _ _ true with "Hs Hbox") as (Pb') "(HP' & EQ & Hbox)".
solve_ndisj. by rewrite lookup_fmap EQB. iDestruct ("HPP'" with "HP'") as "$".
- iApply fupd_mask_intro; [solve_ndisj|]. iIntros "Hclose * HvsQ HQ".
+ iApply fupd_mask_intro; [solve_ndisj|]. iIntros "Hclose %Q HvsQ HQ".
iMod "Hclose" as "_". iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs".
{ iNext. iIntros "HQ H†". iApply "HPP'". iApply ("HvsQ" with "HQ H†"). }
iMod (slice_insert_full _ _ true with "HQ Hbox") as (j) "(% & #Hs' & Hbox)".
--
GitLab