Extend style to other files: more empty lines

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)) ].
 

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.

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 Σ.

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) ].
 

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.

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)].
 

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 Σ.

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 Σ.

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))) ].
 

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))].
 

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.

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.

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.