From e86e16d53a97734a40d6caefeca090bba83688eb Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 21 Dec 2017 16:58:30 +0100
Subject: [PATCH] Fix typo.
---
theories/proofmode/tactics.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 36c2993a7..ffa7bd438 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -399,7 +399,7 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
|match goal with (* Force [A] in [ex_intro] to deal with coercions. *)
| |- ∃ _ : ?A, _ => refine (@ex_intro A _ x (conj _ _)); [|]
(* If the existentially quantified predicate is non-dependent and [x]
- is a hole, [refine] will generate an additional goal it. *)
+ is a hole, [refine] will generate an additional goal. *)
| |- ∃ _ : ?A, _ => refine (@ex_intro A _ x (conj _ _));[shelve| |]
end; [env_reflexivity|go xs]]
end in
--
GitLab