From 3077c6c66f40fa3a358f70de390ce359730935ee Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 9 Aug 2016 13:16:01 +0200
Subject: [PATCH] more spacing fixes for better grouping

---
 program_logic/auth.v       | 3 +--
 program_logic/saved_prop.v | 2 +-
 program_logic/sts.v        | 3 +--
 3 files changed, 3 insertions(+), 5 deletions(-)

diff --git a/program_logic/auth.v b/program_logic/auth.v
index 4dcdf9c7e..a56f54d5b 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -9,9 +9,8 @@ Class authG Σ (A : ucmraT) := AuthG {
   auth_inG :> inG Σ (authR A);
   auth_discrete :> CMRADiscrete A;
 }.
-
-(* The global functor we need and register that they match. *)
 Definition authΣ (A : ucmraT) : gFunctors := #[ GFunctor (constRF (authR A)) ].
+
 Instance subG_authΣ Σ A : subG (authΣ A) Σ → CMRADiscrete A → authG Σ A.
 Proof. intros ?%subG_inG ?. by split. Qed.
 
diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index 4e2888615..0874a7e9f 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -5,9 +5,9 @@ Import uPred.
 
 Class savedPropG (Σ : gFunctors) (F : cFunctor) :=
   saved_prop_inG :> inG Σ (agreeR (laterC (F (iPreProp Σ)))).
-
 Definition savedPropΣ (F : cFunctor) : gFunctors :=
   #[ GFunctor (agreeRF (â–¶ F)) ].
+
 Instance subG_savedPropΣ  {Σ F} : subG (savedPropΣ F) Σ → savedPropG Σ F.
 Proof. apply subG_inG. Qed.
 
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 527780b55..60f34f167 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -8,9 +8,8 @@ Class stsG Σ (sts : stsT) := StsG {
   sts_inG :> inG Σ (stsR sts);
   sts_inhabited :> Inhabited (sts.state sts);
 }.
-
-(* The global functor we need and register that they match. *)
 Definition stsΣ (sts : stsT) : gFunctors := #[ GFunctor (constRF (stsR sts)) ].
+
 Instance subG_stsΣ Σ sts :
   subG (stsΣ sts) Σ → Inhabited (sts.state sts) → stsG Σ sts.
 Proof. intros ?%subG_inG ?. by split. Qed.
-- 
GitLab