From f07fca139e7d5a9982e64cba43be4610ee2ce737 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 15 Oct 2020 14:40:26 +0200
Subject: [PATCH] auth formatting nit

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

diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 13f796c51..b6ea8744f 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -16,7 +16,10 @@ agreement, i.e., [✓ (●{p1} a1 ⋅ ●{p2} a2) → a1 ≡ a2]. *)
 Definition auth_view_rel_raw {A : ucmraT} (n : nat) (a b : A) : Prop :=
   b ≼{n} a ∧ ✓{n} a.
 Lemma auth_view_rel_raw_mono (A : ucmraT) n1 n2 (a1 a2 b1 b2 : A) :
-  auth_view_rel_raw n1 a1 b1 → a1 ≡{n2}≡ a2 → b2 ≼{n2} b1 → n2 ≤ n1 →
+  auth_view_rel_raw n1 a1 b1 →
+  a1 ≡{n2}≡ a2 →
+  b2 ≼{n2} b1 →
+  n2 ≤ n1 →
   auth_view_rel_raw n2 a2 b2.
 Proof.
   intros [??] Ha12 ??. split.
-- 
GitLab