diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 904d30642f2a44faf12c04a8aa4b57be0ffc340a..e283e18deed5bf3226c14dafebfd3c5e97dfdc31 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -900,9 +900,9 @@ Tactic Notation "iNext" open_constr(n) :=
   let P := match goal with |- envs_entails _ ?P => P end in
   try lazymatch n with 0 => fail 1 "iNext: cannot strip 0 laters" end;
   (* apply is sometimes confused wrt. canonical structures search.
-     refine should us the other unification algorithm, which should
+     refine should use the other unification algorithm, which should
      not have this issue. *)
-  notypeclasses refine (coq_tactics.tac_next _ _ n _ _ _ _ _);
+  notypeclasses refine (tac_next _ _ n _ _ _ _ _);
     [apply _ || fail "iNext:" P "does not contain" n "laters"
     |lazymatch goal with
      | |- IntoLaterNEnvs 0 _ _ => fail "iNext:" P "does not contain laters"
@@ -1562,7 +1562,7 @@ Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
 Tactic Notation "iLöbCore" "as" constr (IH) :=
   iStartProof;
   (* apply is sometimes confused wrt. canonical structures search.
-     refine should us the other unification algorithm, which should
+     refine should use the other unification algorithm, which should
      not have this issue. *)
   notypeclasses refine (tac_löb _ _ IH _ _ _ _);
     [reflexivity || fail "iLöb: spatial context not empty, this should not happen"