From 79086c8aa2803ccc0833d482092dcbcfc0fcd763 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 16 Jan 2020 09:46:46 +0100
Subject: [PATCH] Remove some useless newlines.

---
 theories/algebra/list.v | 18 ++++++------------
 theories/bi/big_op.v    | 12 ++++--------
 2 files changed, 10 insertions(+), 20 deletions(-)

diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index e8a433af8..6325e1716 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -21,30 +21,24 @@ Global Instance take_ne : NonExpansive (@take A n) := _.
 Global Instance drop_ne : NonExpansive (@drop A n) := _.
 Global Instance head_ne : NonExpansive (head (A:=A)).
 Proof. destruct 1; by constructor. Qed.
-Global Instance list_lookup_ne i :
-  NonExpansive (lookup (M:=list A) i).
+Global Instance list_lookup_ne i : NonExpansive (lookup (M:=list A) i).
 Proof. intros ????. by apply dist_option_Forall2, Forall2_lookup. Qed.
 Global Instance list_alter_ne n f i :
   Proper (dist n ==> dist n) f →
   Proper (dist n ==> dist n) (alter (M:=list A) f i) := _.
-Global Instance list_insert_ne i :
-  NonExpansive2 (insert (M:=list A) i) := _.
-Global Instance list_inserts_ne i :
-  NonExpansive2 (@list_inserts A i) := _.
-Global Instance list_delete_ne i :
-  NonExpansive (delete (M:=list A) i) := _.
+Global Instance list_insert_ne i : NonExpansive2 (insert (M:=list A) i) := _.
+Global Instance list_inserts_ne i : NonExpansive2 (@list_inserts A i) := _.
+Global Instance list_delete_ne i : NonExpansive (delete (M:=list A) i) := _.
 Global Instance option_list_ne : NonExpansive (@option_list A).
 Proof. intros ????; by apply Forall2_option_list, dist_option_Forall2. Qed.
 Global Instance list_filter_ne n P `{∀ x, Decision (P x)} :
   Proper (dist n ==> iff) P →
   Proper (dist n ==> dist n) (filter (B:=list A) P) := _.
-Global Instance replicate_ne :
-  NonExpansive (@replicate A n) := _.
+Global Instance replicate_ne : NonExpansive (@replicate A n) := _.
 Global Instance reverse_ne : NonExpansive (@reverse A) := _.
 Global Instance last_ne : NonExpansive (@last A).
 Proof. intros ????; by apply dist_option_Forall2, Forall2_last. Qed.
-Global Instance resize_ne n :
-  NonExpansive2 (@resize A n) := _.
+Global Instance resize_ne n : NonExpansive2 (@resize A n) := _.
 
 Lemma list_dist_cons_inv_l n x l k :
   x :: l ≡{n}≡ k → ∃ y k', x ≡{n}≡ y ∧ l ≡{n}≡ k' ∧ k = y :: k'.
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 678f630ca..491596e32 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -906,13 +906,11 @@ Section map2.
   Qed.
   Global Instance big_sepM2_mono' :
     Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊢)))
-      ==> (=) ==> (=) ==> (⊢))
-           (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
+      ==> (=) ==> (=) ==> (⊢)) (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
   Proof. intros f g Hf m1 ? <- m2 ? <-. apply big_sepM2_mono; intros; apply Hf. Qed.
   Global Instance big_sepM2_proper' :
     Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊣⊢)))
-      ==> (=) ==> (=) ==> (⊣⊢))
-           (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
+      ==> (=) ==> (=) ==> (⊣⊢)) (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
   Proof. intros f g Hf m1 ? <- m2 ? <-. apply big_sepM2_proper; intros; apply Hf. Qed.
 
   Lemma big_sepM2_empty Φ : ([∗ map] k↦y1;y2 ∈ ∅; ∅, Φ k y1 y2) ⊣⊢ emp.
@@ -923,15 +921,13 @@ Section map2.
   Lemma big_sepM2_empty' `{BiAffine PROP} P Φ : P ⊢ [∗ map] k↦y1;y2 ∈ ∅;∅, Φ k y1 y2.
   Proof. rewrite big_sepM2_empty. apply (affine _). Qed.
 
-  Lemma big_sepM2_empty_l m1 Φ :
-    ([∗ map] k↦y1;y2 ∈ m1; ∅, Φ k y1 y2) ⊢ ⌜m1 = ∅⌝.
+  Lemma big_sepM2_empty_l m1 Φ : ([∗ map] k↦y1;y2 ∈ m1; ∅, Φ k y1 y2) ⊢ ⌜m1 = ∅⌝.
   Proof.
     rewrite big_sepM2_dom dom_empty_L.
     apply pure_mono, dom_empty_inv_L.
   Qed.
 
-  Lemma big_sepM2_empty_r m2 Φ :
-    ([∗ map] k↦y1;y2 ∈ ∅; m2, Φ k y1 y2) ⊢ ⌜m2 = ∅⌝.
+  Lemma big_sepM2_empty_r m2 Φ : ([∗ map] k↦y1;y2 ∈ ∅; m2, Φ k y1 y2) ⊢ ⌜m2 = ∅⌝.
   Proof.
     rewrite big_sepM2_dom dom_empty_L.
     apply pure_mono=>?. eapply (dom_empty_inv_L (D:=gset K)). eauto.
-- 
GitLab