diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 581c3b63e04c65730390e287d63888a45e766d66..93904be662d5b20cf0c60bb68eca8b126c51a7b7 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -766,7 +766,7 @@ Tactic Notation "iIntoEmpValid" open_constr(t) :=
 [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.
 
-The tactic [iApply] uses laxy type class inference, so that evars can first be
+The tactic [iApply] uses lazy 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.
 *)