From e3a16b576adf5663c6a6150f5d6ecf40047b8784 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 11 Feb 2022 11:15:21 +0100
Subject: [PATCH] Tweaks.

---
 iris/proofmode/coq_tactics.v  | 5 +++--
 iris/proofmode/ltac_tactics.v | 3 ++-
 tests/proofmode.ref           | 2 +-
 tests/proofmode.v             | 4 ++--
 4 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index babf0f783..a2708b041 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 118e5b711..f4da0ed78 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 6e33d033c..ce21d1c9d 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 7eb84f89d..b679d03e1 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 :=
-- 
GitLab