From 3a70b198f5849d95f8d27675f665aa724d70b01e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 30 Aug 2024 13:47:45 +0200
Subject: [PATCH] update dependencies

---
 coq-lambda-rust.opam               | 2 +-
 theories/lifetime/model/creation.v | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 7763ae0a..45c97d81 100644
--- a/coq-lambda-rust.opam
+++ b/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}%"]
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 803eb333..d2954bba 100644
--- a/theories/lifetime/model/creation.v
+++ b/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.
-- 
GitLab