update dependencies

coq-lambda-rust.opam

@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2024-08-16.1.b6462587") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2024-08-30.0.b2983a1e") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]

theories/lifetime/model/creation.v

@@ -75,7 +75,7 @@ Proof.
   { iModIntro. rewrite /Iinv. iFrame.
     iApply (@big_sepS_impl with "[$HK]"); iModIntro.
     iIntros (κ Hκ) "[(_ & _ & %)|[$ _]]". set_solver. }
-  destruct (minimal_exists_L (⊂) Kalive)
+  destruct (minimal_exists_elem_of_L (⊂) Kalive)
     as (κ & [Hκalive HκK]%elem_of_filter & Hκmin); first done.
   iDestruct (@big_sepS_delete with "HK") as "[Hκinv HK]"; first done.
   iDestruct "Hκinv" as "[(Hκ & Hκalive & _)|[_ %]]"; last first.
@@ -114,7 +114,7 @@ Proof.
   induction (set_wf K) as [K _ IH]. iIntros "HK".
   destruct (decide (K = ∅)) as [->|].
   { iExists (λ _, inhabitant). repeat (iSplit; [by auto|]). by rewrite !big_sepS_empty. }
-  destruct (minimal_exists_L (⊂) K) as (κ & HκK & Hκmin); first done.
+  destruct (minimal_exists_elem_of_L (⊂) K) as (κ & HκK & Hκmin); first done.
   rewrite big_sepS_delete //. iDestruct "HK" as "[Hinv HK]".
   iDestruct (IH with "HK") as (Vs) "(Hhv0 & Hmono & HK)". { set_solver +HκK. }
   iDestruct "Hmono" as %Hmono.