diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 3a101a9417c884490c95b2ec4d04f30193f84ad3..a827cbd4e0e6049b7f1337de690ab00cd37724a1 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 d67c547f00d3fda8a7cd957d8d0840f9cedd8bcc..804e47c4e108a97280e571d360dd504cda6d7df3 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 11be5e4ac98a34b55a31aeac1ac540f4c35a5d8d..4da10b23024c601819c3da32d4a65c90d23b4ab5 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 c1d7ea66a9129e208b3b1bf9eb7e2d3ee446784c..50e2c21f0e0ac3f0016c36c85a52aebe3338bdd1 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 cf3e4add51221ecaa03c9c8afc8414c48ad5e764..d2569159fcbec673a18c025620851008b926fc33 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.