diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index f0bcaae772eeb42ed26c00fa1cd3348ab4f52deb..e7b8837e591e7bb801821b5d1b325148554973a1 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 d2691c559e227120b32f1aafdb0274d9814574f1..d9ad06e62595656d63d25315d5970f2084d3802e 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α".