diff --git a/iris/base_logic/lib/ghost_map.v b/iris/base_logic/lib/ghost_map.v
index ea559d567199efc5144a38ca2212d1769cfb42e9..a64159b000da7d33b1d2ae179c3c8c0045623f6d 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 9069f8e3b2b83feb5a735b684e0b7bb4a2c00173..95d6555e1dfe71d49c217097fa12b9e538f2ea31 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 f4fdd230833035df794fd6cfd3fa0746a7abf3f0..c6b701d92c90321c8ad983e0b4baf2df4cecd001 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 29a905c1211b6aec0ba5ddd8c43d6d0f1c276422..2e3a1733904477c0a16c6ca6878a97d6cab28a85 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 c1144c0e19d5cf332f7ea0e838a7a52d1a970c86..da152d3bfb78a02be7c4edf5444d9f2df3698306 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 d89e8bd227349d933e2bddc4eca8093ab9d8416b..cb6312aaccae86bea641bce0511a3d63ec5bb2f3 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 e7fd2a47fc231a855e76886a645316d38874f3ed..70573628927101a2b11bd4b6f6c1a7f5c0a0e93f 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 f1fe32924b4aa2fa97b5d9f06276a8c7910dd75e..6b0ab568bf41dcbe1ce54f43b366fac7abbef558 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 ea3321c70b2f6877ed8ee83efce5f3470306a6d6..c52b35e3d6abfa88c18117c7370a33ae74a80d5e 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 5fa218e562a3a3a0fcf0b35ab2c6bd3f46b04426..6bb43fa67f38b78674d64ec36306d48f44bd10fd 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 4f16c146fb1383a8c2461989ac29e32f51394406..67f4f18e587d1c1783894c625575495a0e717c84 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 f46d470a589b9488d50e753dc8b9b339988a29a1..378177ec1cac857a5ec8462674ea08494500dc5e 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 f2bceed693d43b8de58667a05f3a9b2999f3fc01..506ac4cc71f5ec82f54c09325872fd89242f8e7b 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.