From 84910af8949cac7cfa2be65fdd471253e2440b82 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 31 Jul 2018 21:58:02 +0200
Subject: [PATCH] Fix typo in comment.

---
 theories/proofmode/ltac_tactics.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 581c3b63e..93904be66 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.
 *)
-- 
GitLab