From 59a8f5bfa728caaaab9287e7aa8ed7953392e0a8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 9 Aug 2016 13:10:07 +0200
Subject: [PATCH] better spacing for functor declarations

---
 heap_lang/lib/barrier/proof.v | 5 ++---
 heap_lang/lib/counter.v       | 2 +-
 heap_lang/lib/lock.v          | 2 +-
 heap_lang/lib/spawn.v         | 5 ++---
 heap_lang/lib/ticket_lock.v   | 2 +-
 5 files changed, 7 insertions(+), 9 deletions(-)

diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 3a101a941..a827cbd4e 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -7,15 +7,14 @@ From iris.program_logic Require Import saved_prop sts.
 From iris.heap_lang Require Import proofmode.
 From iris.heap_lang.lib.barrier Require Import protocol.
 
-(** The CMRAs we need. *)
+(** The CMRAs/functors we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
 Class barrierG Σ := BarrierG {
   barrier_stsG :> stsG Σ sts;
   barrier_savedPropG :> savedPropG Σ idCF;
 }.
-(** The Functors we need. *)
 Definition barrierΣ : gFunctors := #[stsΣ sts; savedPropΣ idCF].
-(* Show and register that they match. *)
+
 Instance subG_barrierΣ {Σ} : subG barrierΣ Σ → barrierG Σ.
 Proof. intros [? [? _]%subG_inv]%subG_inv. split; apply _. Qed.
 
diff --git a/heap_lang/lib/counter.v b/heap_lang/lib/counter.v
index d67c547f0..804e47c4e 100644
--- a/heap_lang/lib/counter.v
+++ b/heap_lang/lib/counter.v
@@ -14,8 +14,8 @@ Global Opaque newcounter inc get.
 
 (** The CMRA we need. *)
 Class counterG Σ := CounterG { counter_tokG :> authG Σ mnatUR }.
-
 Definition counterΣ : gFunctors := #[authΣ mnatUR].
+
 Instance subG_counterΣ {Σ} : subG counterΣ Σ → counterG Σ.
 Proof. intros [? _]%subG_inv. split; apply _. Qed.
 
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index 11be5e4ac..4da10b230 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -14,8 +14,8 @@ Global Opaque newlock acquire release.
 (** The CMRA we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
 Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
-
 Definition lockΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
+
 Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
 Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
 
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index c1d7ea66a..50e2c21f0 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -16,12 +16,11 @@ Definition join : val :=
     end.
 Global Opaque spawn join.
 
-(** The CMRA we need. *)
+(** The CMRA & functor we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)
 Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitC) }.
-
-(** The functor we need and register that they match. *)
 Definition spawnΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
+
 Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
 Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
 
diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v
index cf3e4add5..d2569159f 100644
--- a/heap_lang/lib/ticket_lock.v
+++ b/heap_lang/lib/ticket_lock.v
@@ -35,9 +35,9 @@ Class tlockG Σ := TlockG {
    tlock_G :> authG Σ (gset_disjUR nat);
    tlock_exclG  :> inG Σ (exclR unitC)
 }.
-
 Definition tlockΣ : gFunctors :=
   #[authΣ (gset_disjUR nat); GFunctor (constRF (exclR unitC))].
+
 Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
 Proof. intros [? [?%subG_inG _]%subG_inv]%subG_inv. split; apply _. Qed.
 
-- 
GitLab