From e08e5d300a47a45d8ae5dfa9868eee1fb637b6c7 Mon Sep 17 00:00:00 2001
From: Hai Dang <haidang@mpi-sws.org>
Date: Tue, 1 Apr 2025 11:15:45 +0200
Subject: [PATCH] Bump gpfsl
---
coq-lambda-rust.opam | 2 +-
theories/typing/function.v | 6 +++---
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 56dbcbbf..7364120c 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 94fc47be..2cb2dbce 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.
--
GitLab