From c44c38306ece99441b3f665489c827fe29326976 Mon Sep 17 00:00:00 2001
From: Quentin Vermande <quentin.vermande@orange.fr>
Date: Sun, 17 Nov 2024 12:56:36 +0100
Subject: [PATCH] adapt to coq#19822

---
 src/base_logic/lib/wsat.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/base_logic/lib/wsat.v b/src/base_logic/lib/wsat.v
index fcb5fd953..eabee4779 100644
--- a/src/base_logic/lib/wsat.v
+++ b/src/base_logic/lib/wsat.v
@@ -963,7 +963,8 @@ Lemma ownI_bupd_factory_alloc lvl φ Q P :
        ==∗ ∃ i, ⌜φ i⌝ ∗ wsat (S lvl) ∗ ownI_full_bupd_factory lvl i (1/2)%Qp Q P.
 Proof.
   iIntros (?) "(Hw&(HQ&#Hfactory))". iMod (ownI_alloc with "[$Hw HQ]") as (i) "(?&?&?&?)"; eauto; last first.
-  { iModIntro. iExists i. iFrame. instantiate (1:= list_to_vec [Q]). rewrite //=. }
+  { iModIntro. iExists i. iFrame. instantiate (1:= list_to_vec [Q]).
+    (try (iExists 1; iExists [#Q]; iSplit)) => //=. }
   repeat (rewrite ?bi_schema_interp_unfold //=).
   iFrame. eauto.
 Qed.