From 5e328a6977f5ea5bd0b4d66a6b2feabcef195372 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Thu, 31 Aug 2023 13:19:09 +0200
Subject: [PATCH] Remove noise from diff

---
 iris/base_logic/lib/gen_heap.v  | 2 +-
 iris/base_logic/lib/ghost_var.v | 2 +-
 iris/bi/lib/cmra.v              | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/iris/base_logic/lib/gen_heap.v b/iris/base_logic/lib/gen_heap.v
index ec3b3ad28..41f23cb4e 100644
--- a/iris/base_logic/lib/gen_heap.v
+++ b/iris/base_logic/lib/gen_heap.v
@@ -237,7 +237,7 @@ Section gen_heap.
     rewrite meta_unseal /meta_def.
     iIntros "(%γm1 & Hγm1 & Hm1) (%γm2 & Hγm2 & Hm2)".
     iCombine "Hγm1 Hγm2" gives %[_ ->].
-    iCombine "Hm1 Hm2" gives %Hγ. iPureIntro.
+    iCombine "Hm1 Hm2" gives %Hγ; iPureIntro.
     move: Hγ. rewrite -reservation_map_data_op reservation_map_data_valid.
     move=> /to_agree_op_inv_L. naive_solver.
   Qed.
diff --git a/iris/base_logic/lib/ghost_var.v b/iris/base_logic/lib/ghost_var.v
index 30a59b09a..9361c4418 100644
--- a/iris/base_logic/lib/ghost_var.v
+++ b/iris/base_logic/lib/ghost_var.v
@@ -63,7 +63,7 @@ Section lemmas.
     ghost_var γ q1 a1 -∗ ghost_var γ q2 a2 -∗ ⌜a1 = a2⌝.
   Proof.
     iIntros "Hvar1 Hvar2".
-    iDestruct (ghost_var_valid_2 with "Hvar1 Hvar2") as %[_ ->]. done.
+    iDestruct (ghost_var_valid_2 with "Hvar1 Hvar2") as %[_ ?]. done.
   Qed.
 
   Global Instance ghost_var_combine_gives γ a1 q1 a2 q2 :
diff --git a/iris/bi/lib/cmra.v b/iris/bi/lib/cmra.v
index 65fca318a..f3a8b9a20 100644
--- a/iris/bi/lib/cmra.v
+++ b/iris/bi/lib/cmra.v
@@ -149,4 +149,4 @@ Section internal_included_laws.
     + iIntros "[%z Hz]". iRewrite "Hz". by rewrite assoc agree_idemp.
     + iIntros "H". by iExists _.
   Qed.
-End internal_included_laws.
+End internal_included_laws.
\ No newline at end of file
-- 
GitLab