adapt to coq#19822

mit-pdos · Nov 18, 2024 · c44c383 · c44c383
1 parent 828ab2e
commit c44c383
Showing 1 changed file with 2 additions and 1 deletion.
diff --git 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.