diff --git a/tests/fixpoint.v b/tests/fixpoint.v
index d2935202396c1ca67b6f16235480a800ee3b1c0f..b9e3c606fccd3026fbfdb45f9127c8726b2b965a 100644
--- a/tests/fixpoint.v
+++ b/tests/fixpoint.v
@@ -9,7 +9,9 @@ Section fixpoint.
   Definition L := bi_least_fixpoint F.
   Definition G := bi_greatest_fixpoint F.
 
-  (* Make sure the lemmas apply without having to repeat the induction predicate [Φ]. *)
+  (* Make sure the lemmas [iApply] without having to repeat the induction
+  predicate [Φ]. See https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/967
+  for details. *)
   Lemma ind_test (a : A) :
     ∀ x, L x -∗ x ≡ a.
   Proof.