diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 7f90b3dd10fe1503f5cd10cb86293f56d62e8c35..91f06d0a0bcabf854f733168615a70ba7b48daa7 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-01-28.0.6f76c393") | (= "dev") }
+  "coq-gpfsl" { (= "dev.2025-02-05.0.31e913ff") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/arc_cmra.v b/theories/lang/arc_cmra.v
index 7dd05040b4c82781a650a0d43ec1cfbba6894027..b7efaced56e93955525daa46b0aedcc70f330e8c 100644
--- a/theories/lang/arc_cmra.v
+++ b/theories/lang/arc_cmra.v
@@ -549,7 +549,7 @@ Section ArcGhost.
   Qed.
 
   Lemma WeakAuth_valid γ iS st :
-    WeakAuth γ (iS, st) -∗ ⌜st ≠ Some CsumBot⌝.
+    WeakAuth γ (iS, st) -∗ ⌜st ≠ Some CsumInvalid⌝.
   Proof.
     iIntros "own".
     iDestruct (@own_valid _ arcUR with "own") as %[[_ Hvl] _].