From 2da07dc48d7ba917d0cd1a8a0d839fc2e4bfe0f4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Mon, 28 Aug 2023 12:46:51 +0000
Subject: [PATCH] Improve comment.

---
 tests/fixpoint.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/tests/fixpoint.v b/tests/fixpoint.v
index d29352023..b9e3c606f 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.
-- 
GitLab