diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 36c2993a7dbaca50f886570791c80901a75ef4a8..ffa7bd43878e09a06b8287dd4b08c8f7c9317c20 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