diff --git a/program_logic/auth.v b/program_logic/auth.v
index 4dcdf9c7e38fd56214de988ad0a03a43790b64d0..a56f54d5b2e6533e2b15122dc6cb32db4e925339 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 4e2888615d0577ea6b4b0151189dfa5edb5b6a7f..0874a7e9ff2de0553cb18c4ad2585057f2613c55 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 527780b55fdcd0a56dde76b7cf6a56ed05c86bb0..60f34f167ba5be1b95dcc1941227b52dbe1586f4 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.