diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 9aa8bc7668003f14a4b1f67ae228fb75df9c7a64..ad529cf61b68d08729e07a6827e328182e3237a8 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -3325,7 +3325,9 @@ Tactic Notation "iAccu" :=
 Global Hint Extern 0 (_ ⊢ _) => iStartProof : core.
 Global Hint Extern 0 (⊢ _) => iStartProof : core.
 
-(* Make sure that by and done solve trivial things in proof mode *)
+(* Make sure that [by] and [done] solve trivial things in proof mode.
+[iPureIntro] invokes [FromPure], so adding [FromPure] instances can help improve
+what [done] can do. *)
 Global Hint Extern 0 (envs_entails _ _) => iPureIntro; try done : core.
 Global Hint Extern 0 (envs_entails _ ?Q) =>
   first [is_evar Q; fail 1|iAssumption] : core.