From eebd01f90ed4d7106f1139cf58718ea7f5c22dd0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 11 Sep 2024 19:12:44 +0200
Subject: [PATCH] Break long line.

---
 iris/base_logic/lib/ghost_map.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/iris/base_logic/lib/ghost_map.v b/iris/base_logic/lib/ghost_map.v
index e76b96a91..36cdaa1b0 100644
--- a/iris/base_logic/lib/ghost_map.v
+++ b/iris/base_logic/lib/ghost_map.v
@@ -206,7 +206,8 @@ Section lemmas.
     unseal. iIntros "H1 H2".
     (* We need to explicitly specify the Inj instances instead of
     using inj _ since we need to specify [leibnizO] for [to_agree_inj]. *)
-    iCombine "H1 H2" gives %[? ?%(map_fmap_equiv_inj _ (to_agree_inj (A:=(leibnizO _))))]%gmap_view_auth_dfrac_op_valid.
+    iCombine "H1 H2" gives %[? ?%(map_fmap_equiv_inj _
+      (to_agree_inj (A:=(leibnizO _))))]%gmap_view_auth_dfrac_op_valid.
     iPureIntro. split; first done. by fold_leibniz.
   Qed.
   Lemma ghost_map_auth_agree γ q1 q2 m1 m2 :
-- 
GitLab