diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index fe7df1fec0429cb6f3b5f79e6937fb7ab5c361a6..b580a047a07a815e14afba439f98cf1d87fd66af 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -978,7 +978,7 @@ Tactic Notation "iInductionCore" constr(x)
     lazymatch goal with
     | H : coq_tactics.of_envs _ ⊢ _ |- _ =>
        eapply tac_revert_ih;
-         [reflexivity || fail "iInduction: persistent context not empty"
+         [reflexivity || fail "iInduction: spatial context not empty"
          |apply H|];
        clear H; fix_ihs;
        let IH' := iFresh' IH in iIntros [IAlwaysElim (IName IH')]