update dependencies

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}%"]

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 //