diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index e470ea48c3540538e34a64fe87c69283be912819..bc81eba1ede44385c729f7d62fa6c19a79ac5c80 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -570,7 +570,12 @@ Tactic Notation "iIntoValid" open_constr(t) :=
 
 (* The tactic [tac] is called with a temporary fresh name [H]. The argument
 [lazy_tc] denotes whether type class inference on the premises of [lem] should
-be performed before (if false) or after (if true) [tac H] is called. *)
+be performed before (if false) or after (if true) [tac H] is called.
+
+The tactic [iApply] uses laxy type class inference, so that evars can first be
+instantiated by matching with the goal, whereas [iDestruct] does not, because
+eliminations may not be performed when type classes have not been resolved.
+*)
 Tactic Notation "iPoseProofCore" open_constr(lem)
     "as" constr(p) constr(lazy_tc) tactic(tac) :=
   try iStartProof;