From 58864e5b9c643cb3c395ef8f61eea2b2eb0232bc Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Wed, 14 Apr 2021 17:54:07 +0200
Subject: [PATCH] Bump gpfsl
---
coq-lambda-rust.opam | 2 +-
theories/typing/lib/rwlock/rwlockwriteguard_code.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index f0bcaae7..e7b8837e 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.2021-03-07.0.6acef1f1") | (= "dev") }
+ "coq-gpfsl" { (= "dev.2021-04-14.2.89510b36") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index d2691c55..d9ad06e6 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -144,7 +144,7 @@ Section rwlockwriteguard_functions.
iDestruct (GPS_SWWriter_shared with "W") as "[W Rs]".
iSplitR ""; [|done]. iExists None. iSplitL ""; [done|].
iFrame "Share g W Rs". iApply (bor_iff with "[] Hx'").
- iIntros "!> !#". iApply bi_iff_sym. by iApply "EqO". }
+ iIntros "!> !#". iApply bi.iff_sym. by iApply "EqO". }
{ by iIntros "!> !> $". }
iIntros "!>" (?) "(_ & R' & Hβ & _)".
wp_seq. iMod ("Hcloseα" with "Hβ") as "Hα".
--
GitLab