diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index adf16b59dde19df928d6dbc898a54b4a1b2c4a5a..f96e6edf2baa7848d6863ac9d8abd4121be1c930 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -24,7 +24,7 @@ Section core.
   Implicit Types P Q : uPred M.
 
   Lemma coreP_intro P : P -∗ coreP P.
-  Proof. iIntros "HP". by iIntros (Q HQ ->). Qed.
+  Proof. rewrite /coreP. iIntros "HP". by iIntros (Q HQ ->). Qed.
 
   Global Instance coreP_persistent P : PersistentP (coreP P).
   Proof. rewrite /coreP. apply _. Qed.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 06331c5d0ff28ad2181be0f4d755a9841247de4f..d31192a563be1004b54accb126e5e82d0b1d8f2f 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -721,6 +721,32 @@ Global Instance into_forall_always {A} P (Φ : A → uPred M) :
   IntoForall P Φ → IntoForall (□ P) (λ a, □ (Φ a))%I.
 Proof. rewrite /IntoForall=> HP. by rewrite HP always_forall. Qed.
 
+(* FromForall *)
+Global Instance from_forall_forall {A} (Φ : A → uPred M) :
+  FromForall (∀ x, Φ x) Φ.
+Proof. done. Qed.
+Global Instance from_forall_pure {A} (φ : A → Prop) :
+  @FromForall M A (⌜∀ a : A, φ a⌝) (λ a, ⌜ φ a ⌝)%I.
+Proof. by rewrite /FromForall pure_forall. Qed.
+Global Instance from_forall_impl_pure P Q φ :
+  IntoPureT P φ → FromForall (P → Q) (λ _ : φ, Q)%I.
+Proof.
+  intros (φ'&->&?). by rewrite /FromForall -pure_impl_forall (into_pure P).
+Qed.
+Global Instance from_forall_wand_pure P Q φ :
+  IntoPureT P φ → FromForall (P -∗ Q) (λ _ : φ, Q)%I.
+Proof.
+  intros (φ'&->&?). rewrite /FromForall -pure_impl_forall.
+  by rewrite always_impl_wand (into_pure P).
+Qed.
+
+Global Instance from_forall_always {A} P (Φ : A → uPred M) :
+  FromForall P Φ → FromForall (□ P) (λ a, □ (Φ a))%I.
+Proof. rewrite /FromForall=> <-. by rewrite always_forall. Qed.
+Global Instance from_forall_later {A} P (Φ : A → uPred M) :
+  FromForall P Φ → FromForall (▷ P) (λ a, ▷ (Φ a))%I.
+Proof. rewrite /FromForall=> <-. by rewrite later_forall. Qed.
+
 (* FromModal *)
 Global Instance from_modal_later P : FromModal (â–· P) P.
 Proof. apply later_intro. Qed.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 6cabad9ab5ccfbff76016cd631d9729e9d14fe92..caaa47f1784ba14068ee09c3031b249abaaaeb51 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -206,6 +206,11 @@ Class IntoForall {M A} (P : uPred M) (Φ : A → uPred M) :=
 Arguments into_forall {_ _} _ _ {_}.
 Hint Mode IntoForall + - ! - : typeclass_instances.
 
+Class FromForall {M A} (P : uPred M) (Φ : A → uPred M) :=
+  from_forall : (∀ x, Φ x) ⊢ P.
+Arguments from_forall {_ _} _ _ {_}.
+Hint Mode FromForall + - ! - : typeclass_instances.
+
 Class FromModal {M} (P Q : uPred M) := from_modal : Q ⊢ P.
 Arguments from_modal {_} _ _ {_}.
 Hint Mode FromModal + ! - : typeclass_instances.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index f52984b25fff27deac0e4c06823630acbe06e596..50643dd05bb32f515983ff54e1e61a3fa1e245a8 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -512,13 +512,7 @@ Proof.
   rewrite (_ : P = â–¡?false P) // (into_persistentP false P).
   by rewrite right_id always_and_sep_l wand_elim_r.
 Qed.
-Lemma tac_pure_impl_intro Δ (φ ψ : Prop) :
-  (φ → Δ ⊢ ⌜ψ⌝) → Δ ⊢ ⌜φ → ψ⌝.
-Proof. intros. rewrite pure_impl. by apply impl_intro_l, pure_elim_l. Qed.
-Lemma tac_impl_intro_pure Δ P φ Q : IntoPure P φ → (φ → Δ ⊢ Q) → Δ ⊢ P → Q.
-Proof.
-  intros. by apply impl_intro_l; rewrite (into_pure P); apply pure_elim_l.
-Qed.
+
 Lemma tac_impl_intro_drop Δ P Q : (Δ ⊢ Q) → Δ ⊢ P → Q.
 Proof. intros. apply impl_intro_l. by rewrite and_elim_r. Qed.
 
@@ -863,12 +857,11 @@ Proof.
 Qed.
 
 (** * Forall *)
-Lemma tac_forall_intro {A} Δ (Φ : A → uPred M) : (∀ a, Δ ⊢ Φ a) → Δ ⊢ ∀ a, Φ a.
-Proof. apply forall_intro. Qed.
-
-Lemma tac_pure_forall_intro {A} Δ (φ : A → Prop) :
-  (∀ a, Δ ⊢ ⌜φ a⌝) → Δ ⊢ ⌜∀ a, φ a⌝.
-Proof. intros. rewrite pure_forall. by apply forall_intro. Qed.
+Lemma tac_forall_intro {A} Δ (Φ : A → uPred M) Q :
+  FromForall Q Φ →
+  (∀ a, Δ ⊢ Φ a) →
+  Δ ⊢ Q.
+Proof. rewrite /FromForall=> <-. apply forall_intro. Qed.
 
 Lemma tac_forall_specialize {A} Δ Δ' i p P (Φ : A → uPred M) Q :
   envs_lookup i Δ = Some (p, P) → IntoForall P Φ →
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 7d01214b8cd3ad2e3989951e497fd488ff404fbb..5295e6dba1d5c212bbf04e5c42e8d4658cf09a9d 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -284,21 +284,15 @@ Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
 (** * Basic introduction tactics *)
 Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
   try iStartProof;
-  try first
-    [(* (∀ _, _) *) apply tac_forall_intro
-    |(* (?P → _) *) eapply tac_impl_intro_pure;
-      [apply _ ||
-       let P := match goal with |- IntoPure ?P _ => P end in
-       fail "iIntro:" P "not pure"
-      |]
-    |(* (?P -∗ _) *) eapply tac_wand_intro_pure;
+  lazymatch goal with
+  | |- _ ⊢ _ =>
+    eapply tac_forall_intro;
       [apply _ ||
-       let P := match goal with |- IntoPure ?P _ => P end in
-       fail "iIntro:" P "not pure"
-      |]
-    |(* ⌜∀ _, _⌝ *) apply tac_pure_forall_intro
-    |(* ⌜_ → _⌝ *) apply tac_pure_impl_intro];
-  intros x.
+       let P := match goal with |- FromForall ?P _ => P end in
+       fail "iIntro: cannot turn" P "into a universal quantifier"
+      |lazy beta; intros x]
+  | |- _ => intros x
+  end.
 
 Local Tactic Notation "iIntro" constr(H) :=
   iStartProof;
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 28e6152235d7fe8621d91f05e44915c1cf811b57..ef633861b4fc3517ad8df26f5369faa4a70cd740 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -221,6 +221,14 @@ Qed.
 Lemma test_iIntros_let P :
   ∀ Q, let R := True%I in P -∗ R -∗ Q -∗ P ∗ Q.
 Proof. iIntros (Q R) "$ HR $". Qed.
+
+Lemma test_iIntros_modalities P :
+  (□ ▷ ∀ x : nat, ⌜ x = 0 ⌝ -∗ ⌜ x = 0 ⌝ → False -∗ P -∗ P)%I.
+Proof.
+  iIntros (x ??).
+  iIntros "* **". (* Test that fast intros do not work under modalities *)
+  iIntros ([]).
+Qed.
 End tests.
 
 Section more_tests.