diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index babf0f7837a9069a02b801b01c50aa674588cc62..a2708b041d45ae268b9e521448b152e5f32a03b0 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -480,10 +480,11 @@ Note 1: We need an [IntoIH] instance for any predicate transformer (like
 with lists is most common, we currently only support [Forall] and [Forall2].
 
 Note 2: We could also write the instance [into_ih_Forall] using the big operator
-for conjunction, or using the forall quantifier. We use the big operating
+for conjunction, or using the forall quantifier. We use the big operator
 because that corresponds most closely to [Forall], and we use the version with
 separating conjunction because we do not have a binary version of the big
-operator for conjunctions. *)
+operator for conjunctions, and want to treat [Forall] and [Forall2]
+consistently. *)
 Global Instance into_ih_Forall {A} (φ : A → Prop) l Δ Φ :
   (∀ x, IntoIH (φ x) Δ (Φ x)) →
   IntoIH (Forall φ l) Δ ([∗ list] x ∈ l, □ Φ x) | 2.
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 118e5b7115d17ceb26c2b260e1b554a4ba3d6bc4..f4da0ed786ded955e152a2d499e932b067b69484 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -2315,7 +2315,8 @@ Tactic Notation "iInductionCore" tactic3(tac) "as" constr(IH) :=
        notypeclasses refine (tac_revert_ih _ _ _ H _ _ _);
          [iSolveTC ||
           let φ := match goal with |- IntoIH ?φ _ _ => φ end in
-          fail "iInduction: cannot import IH" φ "into proof mode context"
+          fail "iInduction: cannot import IH" φ
+               "into proof mode context (IntoIH instance missing)"
          |pm_reflexivity ||
           fail "iInduction: spatial context not empty, this should not happen"
          |clear H];
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 6e33d033ce56e783e9d0642cbf8ba9cfb34648ac..ce21d1c9d1c2c3b7629c0e461fa8a4ff09977bb1 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -810,4 +810,4 @@ Tactic failure: iInduction: cannot import IH
    (λ t : ntree,
       "H" : ∀ l : list ntree, ([∗ list] x ∈ l, P x) -∗ P (Tree l)
       --------------------------------------â–¡
-      P t) l) into proof mode context.
+      P t) l) into proof mode context (IntoIH instance missing).
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 7eb84f89ddd7c0d1838b47ec0c750428144edd21..b679d03e14ae48a0eba5a29687fb1a936b20cb4a 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1747,8 +1747,8 @@ Section mutual_induction.
     iApply "H". iIntros (x ?). by iApply (big_sepL_elem_of with "IH").
   Qed.
 
-  (** Now let's define a custom version of [Forall], called [my_Forall], and
-  use that in the variant [tree_ind_alt] of the induction principle. The proof
+  (** Now let us define a custom version of [Forall], called [my_Forall], and
+  use that in the variant [ntree_ind_alt] of the induction principle. The proof
   mode does not support [my_Forall], so we test if [iInduction] generates a
   proper error message. *)
   Inductive my_Forall {A} (φ : A → Prop) : list A → Prop :=