diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index 70692eb2ee9eea5d8c8c336cab0cbb339fa15775..1d6be838a1105281889bea8213d2a94bd43d6909 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -713,9 +713,6 @@ Proof.
   by rewrite sep_and intuitionistically_and and_sep_intuitionistically.
 Qed.
 
-(* We use [IsCons] and [IsApp] to make sure that [frame_big_sepL_cons] and
-[frame_big_sepL_app] cannot be applied repeatedly often when having
-[ [∗ list] k ↦ x ∈ ?e, Φ k x] with [?e] an evar. *)
 Global Instance into_sep_big_sepL_cons {A} (Φ : nat → A → PROP) l x l' :
   IsCons l x l' →
   IntoSep ([∗ list] k ↦ y ∈ l, Φ k y)
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 1a3f4043343459629e1a162c2ee7a78c56d8c38c..b4cafc484a13a85fe83123b97f4485d5332b76d2 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -277,6 +277,9 @@ Hint Mode AddModal + - ! ! : typeclass_instances.
 Lemma add_modal_id {PROP : bi} (P Q : PROP) : AddModal P P Q.
 Proof. by rewrite /AddModal wand_elim_r. Qed.
 
+(** We use the classes [IsCons] and [IsApp] to make sure that instances such as
+[frame_big_sepL_cons] and [frame_big_sepL_app] cannot be applied repeatedly
+often when having [ [∗ list] k ↦ x ∈ ?e, Φ k x] with [?e] an evar. *)
 Class IsCons {A} (l : list A) (x : A) (k : list A) := is_cons : l = x :: k.
 Class IsApp {A} (l k1 k2 : list A) := is_app : l = k1 ++ k2.
 Global Hint Mode IsCons + ! - - : typeclass_instances.