From f063ea939a0c10464b7c2a0099ed278602f64b69 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Wed, 2 Mar 2022 00:57:26 +0100
Subject: [PATCH] Extend style to other files: more empty lines

---
 iris/base_logic/lib/ghost_map.v     | 1 +
 iris/base_logic/lib/mono_nat.v      | 1 +
 iris/base_logic/lib/na_invariants.v | 1 +
 iris/base_logic/lib/saved_prop.v    | 1 +
 iris_deprecated/base_logic/auth.v   | 1 +
 iris_heap_lang/lib/counter.v        | 2 ++
 iris_heap_lang/lib/spawn.v          | 1 +
 iris_heap_lang/lib/spin_lock.v      | 1 +
 iris_heap_lang/lib/ticket_lock.v    | 1 +
 iris_staging/base_logic/mono_list.v | 1 +
 tests/ipm_paper.v                   | 1 +
 tests/one_shot.v                    | 1 +
 tests/one_shot_once.v               | 1 +
 13 files changed, 14 insertions(+)

diff --git a/iris/base_logic/lib/ghost_map.v b/iris/base_logic/lib/ghost_map.v
index ea559d567..a64159b00 100644
--- a/iris/base_logic/lib/ghost_map.v
+++ b/iris/base_logic/lib/ghost_map.v
@@ -15,6 +15,7 @@ Class ghost_mapG Σ (K V : Type) `{Countable K} := GhostMapG {
   ghost_map_inG : inG Σ (gmap_viewR K (leibnizO V));
 }.
 Local Existing Instance ghost_map_inG.
+
 Definition ghost_mapΣ (K V : Type) `{Countable K} : gFunctors :=
   #[ GFunctor (gmap_viewR K (leibnizO V)) ].
 
diff --git a/iris/base_logic/lib/mono_nat.v b/iris/base_logic/lib/mono_nat.v
index 9069f8e3b..95d6555e1 100644
--- a/iris/base_logic/lib/mono_nat.v
+++ b/iris/base_logic/lib/mono_nat.v
@@ -16,6 +16,7 @@ From iris.prelude Require Import options.
 Class mono_natG Σ :=
   MonoNatG { mono_natG_inG : inG Σ mono_natR; }.
 Local Existing Instance mono_natG_inG.
+
 Definition mono_natΣ : gFunctors := #[ GFunctor mono_natR ].
 Global Instance subG_mono_natΣ Σ : subG mono_natΣ Σ → mono_natG Σ.
 Proof. solve_inG. Qed.
diff --git a/iris/base_logic/lib/na_invariants.v b/iris/base_logic/lib/na_invariants.v
index f4fdd2308..c6b701d92 100644
--- a/iris/base_logic/lib/na_invariants.v
+++ b/iris/base_logic/lib/na_invariants.v
@@ -11,6 +11,7 @@ Definition na_inv_pool_name := gname.
 Class na_invG Σ :=
   na_inv_inG : inG Σ (prodR coPset_disjR (gset_disjR positive)).
 Local Existing Instance na_inv_inG.
+
 Definition na_invΣ : gFunctors :=
   #[ GFunctor (constRF (prodR coPset_disjR (gset_disjR positive))) ].
 Global Instance subG_na_invG {Σ} : subG na_invΣ Σ → na_invG Σ.
diff --git a/iris/base_logic/lib/saved_prop.v b/iris/base_logic/lib/saved_prop.v
index 29a905c12..2e3a17339 100644
--- a/iris/base_logic/lib/saved_prop.v
+++ b/iris/base_logic/lib/saved_prop.v
@@ -13,6 +13,7 @@ Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
   saved_anything_contractive : oFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
 }.
 Local Existing Instance saved_anything_inG.
+
 Definition savedAnythingΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
   #[ GFunctor (agreeRF F) ].
 
diff --git a/iris_deprecated/base_logic/auth.v b/iris_deprecated/base_logic/auth.v
index c1144c0e1..da152d3bf 100644
--- a/iris_deprecated/base_logic/auth.v
+++ b/iris_deprecated/base_logic/auth.v
@@ -15,6 +15,7 @@ Class authG Σ (A : ucmra) := AuthG {
   auth_cmra_discrete :> CmraDiscrete A;
 }.
 Local Existing Instance auth_inG.
+
 Definition authΣ (A : ucmra) : gFunctors := #[ GFunctor (authR A) ].
 
 Global Instance subG_authΣ Σ A : subG (authΣ A) Σ → CmraDiscrete A → authG Σ A.
diff --git a/iris_heap_lang/lib/counter.v b/iris_heap_lang/lib/counter.v
index d89e8bd22..cb6312aac 100644
--- a/iris_heap_lang/lib/counter.v
+++ b/iris_heap_lang/lib/counter.v
@@ -15,6 +15,7 @@ Definition read : val := λ: "l", !"l".
 (** Monotone counter *)
 Class mcounterG Σ := MCounterG { mcounter_inG : inG Σ (authR max_natUR) }.
 Local Existing Instance mcounter_inG.
+
 Definition mcounterΣ : gFunctors := #[GFunctor (authR max_natUR)].
 
 Global Instance subG_mcounterΣ {Σ} : subG mcounterΣ Σ → mcounterG Σ.
@@ -89,6 +90,7 @@ End mono_proof.
 Class ccounterG Σ :=
   CCounterG { ccounter_inG : inG Σ (frac_authR natR) }.
 Local Existing Instance ccounter_inG.
+
 Definition ccounterΣ : gFunctors :=
   #[GFunctor (frac_authR natR)].
 
diff --git a/iris_heap_lang/lib/spawn.v b/iris_heap_lang/lib/spawn.v
index e7fd2a47f..705736289 100644
--- a/iris_heap_lang/lib/spawn.v
+++ b/iris_heap_lang/lib/spawn.v
@@ -21,6 +21,7 @@ Definition join : val :=
 (* Not bundling heapGS, as it may be shared with other users. *)
 Class spawnG Σ := SpawnG { spawn_tokG : inG Σ (exclR unitO) }.
 Local Existing Instance spawn_tokG.
+
 Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO)].
 
 Global Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v
index f1fe32924..6b0ab568b 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -16,6 +16,7 @@ Definition release : val := λ: "l", "l" <- #false.
 (* Not bundling heapGS, as it may be shared with other users. *)
 Class lockG Σ := LockG { lock_tokG : inG Σ (exclR unitO) }.
 Local Existing Instance lock_tokG.
+
 Definition lockΣ : gFunctors := #[GFunctor (exclR unitO)].
 
 Global Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
diff --git a/iris_heap_lang/lib/ticket_lock.v b/iris_heap_lang/lib/ticket_lock.v
index ea3321c70..c52b35e3d 100644
--- a/iris_heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -30,6 +30,7 @@ Definition release : val :=
 Class tlockG Σ :=
   tlock_G : inG Σ (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat))).
 Local Existing Instance tlock_G.
+
 Definition tlockΣ : gFunctors :=
   #[ GFunctor (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat))) ].
 
diff --git a/iris_staging/base_logic/mono_list.v b/iris_staging/base_logic/mono_list.v
index 5fa218e56..6bb43fa67 100644
--- a/iris_staging/base_logic/mono_list.v
+++ b/iris_staging/base_logic/mono_list.v
@@ -24,6 +24,7 @@ From iris.prelude Require Import options.
 Class mono_listG (A : Type) Σ :=
   MonoListG { mono_list_inG : inG Σ (mono_listR (leibnizO A)) }.
 Local Existing Instance mono_list_inG.
+
 Definition mono_listΣ (A : Type) : gFunctors :=
   #[GFunctor (mono_listR (leibnizO A))].
 
diff --git a/tests/ipm_paper.v b/tests/ipm_paper.v
index 4f16c146f..67f4f18e5 100644
--- a/tests/ipm_paper.v
+++ b/tests/ipm_paper.v
@@ -190,6 +190,7 @@ End M.
 
 Class counterG Σ := CounterG { counter_tokG : inG Σ M_UR }.
 Local Existing Instance counter_tokG.
+
 Definition counterΣ : gFunctors := #[GFunctor (constRF M_UR)].
 Global Instance subG_counterΣ {Σ} : subG counterΣ Σ → counterG Σ.
 Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
diff --git a/tests/one_shot.v b/tests/one_shot.v
index f46d470a5..378177ec1 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -33,6 +33,7 @@ Definition Shot (n : Z) : one_shotR := Cinr (to_agree n).
 
 Class one_shotG Σ := { one_shot_inG : inG Σ one_shotR }.
 Local Existing Instance one_shot_inG.
+
 Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
 Global Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
 Proof. solve_inG. Qed.
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index f2bceed69..506ac4cc7 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -30,6 +30,7 @@ Definition Shot (n : Z) : one_shotR := Cinr (to_agree n).
 
 Class one_shotG Σ := { one_shot_inG : inG Σ one_shotR }.
 Local Existing Instance one_shot_inG.
+
 Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
 Global Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
 Proof. solve_inG. Qed.
-- 
GitLab