Bump gpfsl

coq-lambda-rust.opam

@@ -15,7 +15,7 @@ This branch uses a proper weak memory model.
 """
 
 depends: [
-  "coq-gpfsl" { (= "dev.2025-03-28.1.ae415dea") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2025-03-31.0.8e4abbc0") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]

theories/typing/function.v

@@ -174,10 +174,10 @@ Section typing.
     iDestruct ("Hcons" with "[$]") as "#(HE & Htys & Hty)".
     iApply ("Hf" with "LFT HE Htl HL [HC] [HT]").
     - unfold cctx_interp. iIntros (elt) "Helt".
-      iDestruct "Helt" as %->%stdpp.list.elem_of_list_singleton. iIntros (ret) "Htl HL HT".
+      iDestruct "Helt" as %->%elem_of_list_singleton. iIntros (ret) "Htl HL HT".
       unfold cctx_elt_interp.
       iApply ("HC" $! (_ ◁cont(_, _)) with "[%] Htl HL [> -]").
-      { by apply stdpp.list.elem_of_list_singleton. }
+      { by apply elem_of_list_singleton. }
       rewrite /tctx_interp !big_sepL_singleton /=.
       iDestruct "HT" as (v) "[HP Hown]". iExists v. iFrame "HP".
       iDestruct (box_type_incl with "[$Hty]") as "(_ & #Hincl & _)".
@@ -341,7 +341,7 @@ Section typing.
     iMod (lctx_lft_alive_tok_list _ _ κs with "HE HL") as (q) "(Hκs & HL & Hclose)"; [done..|].
     iApply (type_call_iris' with "LFT HE Htl HL Hκs Hf Hargs"); [done|].
     iIntros (r) "Htl HL Hκs Hret". iMod ("Hclose" with "Hκs HL") as "HL".
-    iSpecialize ("HC" with "[]"); first by (iPureIntro; apply stdpp.list.elem_of_list_singleton).
+    iSpecialize ("HC" with "[]"); first by (iPureIntro; apply elem_of_list_singleton).
     iApply ("HC" $! [#r] with "Htl HL").
     rewrite tctx_interp_cons tctx_hasty_val. iFrame.
   Qed.