From ac963c1128929bcca8e9bfac8b13107a3889cd5a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 4 Oct 2023 07:26:05 +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 99df3cd0..1a16b6ab 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.2023-09-30.0.941e58fb") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2023-10-03.0.41e501bd") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lifetime/model/creation.v b/theories/lifetime/model/creation.v
index 2281b1a7..803eb333 100644
--- a/theories/lifetime/model/creation.v
+++ b/theories/lifetime/model/creation.v
@@ -81,7 +81,7 @@ Proof.
   iDestruct "Hκinv" as "[(Hκ & Hκalive & _)|[_ %]]"; last first.
   { by destruct (lft_alive_and_dead_in A κ). }
   assert (κ ∉ K') as HκK' by set_solver +HκK HKK'.
-  specialize (IH (K ∖ {[ κ ]})). feed specialize IH; [set_solver +HκK|set_solver +HVs|].
+  ospecialize (IH (K ∖ {[ κ ]}) _ _); [set_solver +HκK|set_solver +HVs|].
   iMod (IH ({[ κ ]} ∪ K') with "[HI Halive Hκalive] HK") as "[[HI Halive] Hdead]".
   { set_solver +HKK'. }
   { rewrite [_ ∪ K'](comm (R:=eq)) -(assoc (R:=eq) (∪)) -union_difference_L //
-- 
GitLab