From 3003fedbc4d744e14cb40da37e2e759b27da02bf Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 14 May 2022 08:45:20 +0200
Subject: [PATCH] update dependencies

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

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index dc8d1118..915d6d3b 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.2022-05-13.2.6902a72f") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2022-05-15.0.67fb1a52") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 3c375ab2..52ac3b87 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -161,7 +161,7 @@ Lemma lft_create_strong P E :
 Proof.
   assert (userE_lftN_disj:=userE_lftN_disj). iIntros (HP ?) "#LFT".
   iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose".
-  rewrite ->pred_infinite_set in HP.
+  rewrite ->(pred_infinite_set (C:=gset _)) in HP.
   destruct (HP (dom A)) as [Λ [HPx HΛ%not_elem_of_dom]].
   iMod (own_update with "HA") as "[HA HΛ]".
   { apply auth_update_alloc, (alloc_singleton_local_update _ Λ
-- 
GitLab