From a06be68ed9a2dd05f6ae7253b62aaaff4e8c30f6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 28 Aug 2023 13:56:17 +0000
Subject: [PATCH] remove spurious space

---
 iris_heap_lang/lib/rw_lock.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris_heap_lang/lib/rw_lock.v b/iris_heap_lang/lib/rw_lock.v
index 2350e14a6..35aa7886e 100644
--- a/iris_heap_lang/lib/rw_lock.v
+++ b/iris_heap_lang/lib/rw_lock.v
@@ -35,7 +35,7 @@ Class rwlock `{!heapGS_gen hlc Σ} := RwLock {
   (** * General properties of the predicates *)
   is_rw_lock_persistent γ lk Φ :> Persistent (is_rw_lock γ lk Φ);
   is_rw_lock_iff γ lk Φ Ψ :
-    is_rw_lock γ lk Φ -∗ ▷ □ (∀ q,  Φ q ∗-∗ Ψ q) -∗ is_rw_lock γ lk Ψ;
+    is_rw_lock γ lk Φ -∗ ▷ □ (∀ q, Φ q ∗-∗ Ψ q) -∗ is_rw_lock γ lk Ψ;
   reader_locked_timeless γ q :> Timeless (reader_locked γ q);
   writer_locked_timeless γ :> Timeless (writer_locked γ);
   writer_locked_exclusive γ : writer_locked γ -∗ writer_locked γ -∗ False;
-- 
GitLab