diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index e48d17176c9275f4be9cf15a9a5a15ae1d72f1b5..83a56109cd5fac6fe44e67a7fa3fc838bc98358c 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -982,7 +982,7 @@ Tactic Notation "iModIntro" uconstr(sel) :=
      | MIEnvIsEmpty => fail "iModIntro: persistent context is non-empty"
      end
     |iSolveTC ||
-     let s := lazymatch goal with |- IntoModalPersistentEnv _ _ _ ?s => s end in
+     let s := lazymatch goal with |- IntoModalSpatialEnv _ _ _ ?s _ => s end in
      lazymatch eval hnf in s with
      | MIEnvForall ?C => fail "iModIntro: spatial context does not satisfy" C
      | MIEnvIsEmpty => fail "iModIntro: spatial context is non-empty"