From 3a6eafbba7e40a4fd6cd9683d061034b11233ce8 Mon Sep 17 00:00:00 2001
From: Hai Dang <haidang@mpi-sws.org>
Date: Sun, 26 Jan 2025 18:56:36 +0100
Subject: [PATCH] fix to be compatible with coq 9.0+rc1

---
 gpfsl/logic/relacq.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/gpfsl/logic/relacq.v b/gpfsl/logic/relacq.v
index d7dc2427..344530b5 100644
--- a/gpfsl/logic/relacq.v
+++ b/gpfsl/logic/relacq.v
@@ -55,7 +55,6 @@ Section RelAcqProp.
   Proof.
     unseal. iIntros "obj".
     iExists ∅. rewrite -view_at_objectively. iFrame "obj".
-    rewrite (_: (◯ to_latT (∅: threadView) : authR _) = ε) //.
     rewrite -embed_bupd. by iApply own_unit.
   Qed.
 
-- 
GitLab