From d68378bfe6a50dca812eced02a412f5c8be6f71a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 2 Nov 2020 08:41:53 +0100
Subject: [PATCH] Line break.

---
 theories/bi/big_op.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 5f2bc2e77..a084702a0 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -1704,7 +1704,10 @@ Section gmultiset.
 
   Lemma big_sepMS_subseteq `{BiAffine PROP} Φ X Y :
     Y ⊆ X → ([∗ mset] x ∈ X, Φ x) ⊢ [∗ mset] x ∈ Y, Φ x.
-  Proof. rewrite big_opMS_eq. intros. by apply big_sepL_submseteq, gmultiset_elements_submseteq. Qed.
+  Proof.
+    intros. rewrite big_opMS_eq.
+    by apply big_sepL_submseteq, gmultiset_elements_submseteq.
+  Qed.
 
   (** The lemmas [big_sepMS_mono], [big_sepMS_ne] and [big_sepMS_proper] are more
   generic than the instances as they also give [l !! k = Some y] in the premise. *)
-- 
GitLab