diff --git a/iris/proofmode/class_instances_later.v b/iris/proofmode/class_instances_later.v
index 09d0cf4d01eae8be370a78814894d0ad361bf69c..c27ebf69d36e87fec03296b07bf929021a8b7bdc 100644
--- a/iris/proofmode/class_instances_later.v
+++ b/iris/proofmode/class_instances_later.v
@@ -282,6 +282,10 @@ Global Instance into_laterN_later only_head n n' m' P Q lQ :
   progress, but there may still be a left-over (i.e. [n']) to cancel more deeply
   into [P], as such, we continue with [MaybeIntoLaterN]. *)
   TCIf (TCEq 1 m') (IntoLaterN only_head n' P Q) (MaybeIntoLaterN only_head n' P Q) →
+  (* Similar to [iFrame], the [iNext] tactic also performs a traversal through a
+  term (a hypothesis) to find laters to strip. And like [iFrame] we don't want
+  this to be excessively smart. So we use the same typeclass as [iFrame] here.
+  *)
   MakeLaterN m' Q lQ →
   IntoLaterN only_head n (â–· P) lQ | 2.
 Proof.