diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 56dbcbbf7122cf5a5d9657392f26b1e5528af84f..7364120c5adc9fe9145792f7dd5a15c108ce5eaf 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.2025-03-28.1.ae415dea") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2025-03-31.0.8e4abbc0") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 94fc47bee46c79411c681dd6e9b2704ca25cf836..2cb2dbce2137820f19a063f38f11426d7fd80b75 100644
--- a/theories/typing/function.v
+++ b/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.