From 8da58b7f25c80bb3cd74740b2eb0f1644dd5d08f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 18 Feb 2019 13:12:48 +0100
Subject: [PATCH] linebreaks for readability

---
 theories/algebra/gmap.v | 4 +++-
 theories/algebra/gset.v | 3 ++-
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index 9b194ac4f..1f402b14e 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -306,7 +306,9 @@ Lemma insert_op m1 m2 i x y :
 Proof. by rewrite (insert_merge (â‹…) m1 m2 i (x â‹… y) x y). Qed.
 
 Lemma insert_updateP (P : A → Prop) (Q : gmap K A → Prop) m i x :
-  x ~~>: P → (∀ y, P y → Q (<[i:=y]>m)) → <[i:=x]>m ~~>: Q.
+  x ~~>: P →
+  (∀ y, P y → Q (<[i:=y]>m)) →
+  <[i:=x]>m ~~>: Q.
 Proof.
   intros Hx%option_updateP' HP; apply cmra_total_updateP=> n mf Hm.
   destruct (Hx n (Some (mf !! i))) as ([y|]&?&?); try done.
diff --git a/theories/algebra/gset.v b/theories/algebra/gset.v
index b4d5e520d..83d923854 100644
--- a/theories/algebra/gset.v
+++ b/theories/algebra/gset.v
@@ -134,7 +134,8 @@ Section gset_disj.
 
   Lemma gset_disj_alloc_updateP_strong P (Q : gset_disj K → Prop) X :
     (∀ Y, X ⊆ Y → ∃ j, j ∉ Y ∧ P j) →
-    (∀ i, i ∉ X → P i → Q (GSet ({[i]} ∪ X))) → GSet X ~~>: Q.
+    (∀ i, i ∉ X → P i → Q (GSet ({[i]} ∪ X))) →
+    GSet X ~~>: Q.
   Proof.
     intros Hfresh HQ.
     apply cmra_discrete_updateP=> ? /gset_disj_valid_inv_l [Y [->?]].
-- 
GitLab