From 03135b130a4fad0e99fa5375a03b1ee4b3175ec0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 5 Feb 2025 08:40:56 +0100
Subject: [PATCH] update dependencies

---
 coq-lambda-rust.opam     | 2 +-
 theories/lang/arc_cmra.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 7f90b3dd..91f06d0a 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 7dd05040..b7efaced 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] _].
-- 
GitLab