diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4fe7fcb46ab6b6a9178f1ef39e04afc40354773b..5fab43e3153b408e8cb5a7d8719ac726129780b9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -20,6 +20,10 @@ lemma.
 * Change `iInduction` to always generate a magic wand instead of sometimes
   generating an implication for reverted hypotheses.
 * Add `iUnfold` tactic.
+* Improve ability to name induction hypotheses (IHs) in `iInduction`: when
+  performing `iInduction x as cpat` the names of the IHs in the Coq introduction
+  pattern `cpat` are used to name the IHs in the proof mode context. For
+  example, `iInduction n as [|n IH]` and `iInduction t as [|l IHl r IHr]`.
 
 **Changes in `base_logic`:**
 
diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index 4363ddbc4933f82e6f3109245f59944de6068e2f..4407a6cd1379c49837974667139206f3b35d5b50 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -240,18 +240,26 @@ Induction
   + `iLöb as "IH" forall (x1 ... xn) "selpat"` : perform Löb induction,
   generalizing over the Coq level variables `x1 ... xn`, the hypotheses given by
   the selection pattern `selpat`, and the spatial context as usual.
-- `iInduction x as cpat "IH" "selpat"` : perform induction on
-  the Coq term `x`. The Coq introduction pattern `cpat` is used to name the introduced
-  variables. The induction hypotheses are inserted into the intuitionistic
-  context and given fresh names prefixed `IH`.
-  + `iInduction x as cpat "IH" forall (x1 ... xn) "selpat"` : perform induction,
+- `iInduction x as cpat` : perform induction on the Coq term `x`. The
+  Coq introduction pattern `cpat` is used to name the introduced variables,
+  including the induction hypotheses which are introduced into the proof mode
+  context. Note that induction hypotheses should not be put into string
+  quotation marks `".."`, e.g., use `iInduction n as [|n IH]` to perform
+  induction on a natural number `n`. An implementation caveat is that the names
+  of the induction hypotheses should be fresh in both the Coq context and the
+  proof mode context.
+  + `iInduction x as cpat forall (x1 ... xn) "selpat"` : perform induction,
     generalizing over the Coq level variables `x1 ... xn`, the hypotheses given by
     the selection pattern `selpat`, and the spatial context.
-  + `iInduction x as cpat "IH" using t` : perform induction using the induction
+  + `iInduction x as cpat using t` : perform induction using the induction
     scheme `t`. Common examples of induction schemes are `map_ind`, `set_ind_L`,
     and `gmultiset_ind` for `gmap`, `gset`, and `gmultiset`.
-  + `iInduction x as cpat "IH" using t forall (x1 ... xn) "selpat"` : the above
+  + `iInduction x as cpat using t forall (x1 ... xn) "selpat"` : the above
     variants combined.
+  + `iInduction x as cpat "IH" "selpat"` : ignore the names of the induction
+    hypotheses from `cpat` and call them `IH`, `IH1`, `IH2`, etc. Here "IH" is
+    a string (in string quotation marks). This is *legacy* syntax that might be
+    deprecated in the future. Similar legacy syntax exists for all variants above.
 
 Rewriting / simplification
 --------------------------
diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
index bcc7f3311bdf06f5a7d5d07687092854af340dcf..8f08f6c30564844c9894307c45a795ab2b28ec01 100644
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
@@ -379,7 +379,7 @@ Module le_upd.
     iPoseProof (H C) as "Hc". iSpecialize ("Hc" with "Hâ—¯").
     iPoseProof (le_upd_elim_complete m with "H● Hc") as "H".
     simpl. iMod "H". iModIntro. iNext.
-    clear H. iInduction m as [|m] "IH"; simpl; [done|].
+    clear H. iInduction m as [|m IH]; simpl; [done|].
     iMod "H". iNext. by iApply "IH".
   Qed.
 End le_upd.
diff --git a/iris/bi/lib/relations.v b/iris/bi/lib/relations.v
index be4223c7271ebb1bcec801d8af91d9e378b7bac6..6724d87191c8356ed94d482379f807a53e008aff 100644
--- a/iris/bi/lib/relations.v
+++ b/iris/bi/lib/relations.v
@@ -306,7 +306,7 @@ Section general.
   Lemma bi_nsteps_trans n m x y z :
     bi_nsteps R n x y -∗ bi_nsteps R m y z -∗ bi_nsteps R (n + m) x z.
   Proof.
-    iInduction n as [|n] "IH" forall (x); simpl.
+    iInduction n as [|n IH] forall (x); simpl.
     - iIntros "Heq". iRewrite "Heq". auto.
     - iDestruct 1 as (x') "[Hxx' Hx'y]". iIntros "Hyz".
       iExists x'. iFrame "Hxx'". iApply ("IH" with "Hx'y Hyz").
@@ -323,7 +323,7 @@ Section general.
   Lemma bi_nsteps_add_inv n m x z :
     bi_nsteps R (n + m) x z ⊢ ∃ y, bi_nsteps R n x y ∗ bi_nsteps R m y z.
   Proof.
-    iInduction n as [|n] "IH" forall (x).
+    iInduction n as [|n IH] forall (x).
     - iIntros "Hxz". iExists x. auto.
     - iDestruct 1 as (y) "[Hxy Hyz]".
       iDestruct ("IH" with "Hyz") as (y') "[Hyy' Hy'z]".
@@ -368,7 +368,7 @@ Section general.
       iExists (S n). iSplitR; first auto with lia.
       iApply (bi_nsteps_l with "Hxx' Hx'y").
     - iDestruct 1 as (n ?) "Hxy".
-      iInduction n as [|n] "IH" forall (y). { lia. }
+      iInduction n as [|n IH] forall (y). { lia. }
       rewrite bi_nsteps_inv_r.
       iDestruct "Hxy" as (x') "[Hxx' Hx'y]".
       destruct n.
@@ -387,7 +387,7 @@ Section general.
       iDestruct "IH" as (n) "Hx'y".
       iExists (S n). iApply (bi_nsteps_l with "Hxx' Hx'y").
     - iDestruct 1 as (n) "Hxy".
-      iInduction n as [|n] "IH" forall (y).
+      iInduction n as [|n IH] forall (y).
       { simpl. iRewrite "Hxy". iApply bi_rtc_refl. }
       iDestruct (bi_nsteps_inv_r with "Hxy") as (x') "[Hxx' Hx'y]".
       iApply (bi_rtc_r with "[Hxx'] Hx'y").
diff --git a/iris/program_logic/lifting.v b/iris/program_logic/lifting.v
index 5bcd190ea6c99910b48cbc3b34eb160f1b637231..06018dad005a3c0885107f86660042eb8c872cfa 100644
--- a/iris/program_logic/lifting.v
+++ b/iris/program_logic/lifting.v
@@ -159,7 +159,7 @@ Lemma wp_pure_step_fupd `{!Inhabited (state Λ)} s E E' e1 e2 φ n Φ :
   (|={E}[E']▷=>^n £ n -∗ WP e2 @ s; E {{ Φ }}) ⊢ WP e1 @ s; E {{ Φ }}.
 Proof.
   iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
-  iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl.
+  iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?] ? IH]; simpl.
   { iMod lc_zero as "Hz". by iApply "Hwp". }
   iApply wp_lift_pure_det_step_no_fork.
   - intros σ. specialize (Hsafe σ). destruct s; eauto using reducible_not_val.
diff --git a/iris/program_logic/total_adequacy.v b/iris/program_logic/total_adequacy.v
index 17ce1bda35fe346ea156ffebefca8a00695dc634..526cb85e3dfbf77c7f037336c5128e9bfdb7e1c6 100644
--- a/iris/program_logic/total_adequacy.v
+++ b/iris/program_logic/total_adequacy.v
@@ -98,7 +98,7 @@ Proof.
   iMod ("IH" with "[% //]") as "($ & Hσ & [IH _] & IHfork)".
   iModIntro. iExists (length efs + nt). iFrame "Hσ".
   iApply (twptp_app [_] with "(IH [//])").
-  clear. iInduction efs as [|e efs] "IH"; simpl.
+  clear. iInduction efs as [|e efs IH]; simpl.
   { rewrite twptp_unfold /twptp_pre. iIntros (t2 σ1 ns κ κs σ2 nt1 Hstep).
     destruct Hstep; simplify_eq/=; discriminate_list. }
   iDestruct "IHfork" as "[[IH' _] IHfork]".
diff --git a/iris/program_logic/total_lifting.v b/iris/program_logic/total_lifting.v
index 8502c624029808732fb62e2bff4e2e3dfac71457..35353ae8a0c99fd580cfb379813ce06572a5db7c 100644
--- a/iris/program_logic/total_lifting.v
+++ b/iris/program_logic/total_lifting.v
@@ -82,7 +82,7 @@ Lemma twp_pure_step `{!Inhabited (state Λ)} s E e1 e2 φ n Φ :
   WP e2 @ s; E [{ Φ }] ⊢ WP e1 @ s; E [{ Φ }].
 Proof.
   iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
-  iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
+  iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?] ? IH]; simpl; first done.
   iApply twp_lift_pure_det_step_no_fork; [done|naive_solver|].
   iModIntro. by iApply "IH".
 Qed.
diff --git a/iris/program_logic/weakestpre.v b/iris/program_logic/weakestpre.v
index 8e8e796b06fd0c7fc1999963e14cf5cd8b96acdb..e9623aa7ee76ed65e61f1b3fc177ba24da65f9a4 100644
--- a/iris/program_logic/weakestpre.v
+++ b/iris/program_logic/weakestpre.v
@@ -265,7 +265,7 @@ Proof.
   iIntros "!>" (e2 σ2 efs Hstep) "Hcred". iMod ("H" $! e2 σ2 efs with "[% //] Hcred") as "H".
   iIntros "!>!>". iMod "H". iMod "HP". iModIntro.
   revert n Hn. generalize (num_laters_per_step ns)=>n0 n Hn.
-  iInduction n as [|n] "IH" forall (n0 Hn).
+  iInduction n as [|n IH] forall (n0 Hn).
   - iApply (step_fupdN_wand with "H"). iIntros ">($ & Hwp & $)". iMod "HP".
     iModIntro. iApply (wp_strong_mono with "Hwp"); [done|set_solver|].
     iIntros (v) "HΦ". iApply ("HΦ" with "HP").
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 2bb82176f0354d4544cc824c434d61d112ddc7ba..95453c55be896474414a38cb310729876f586e66 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1732,7 +1732,11 @@ result in the following actions:
 - Introduce the pure hypotheses [x1..xn]
 - Introduce the spatial hypotheses and intuitionistic hypotheses involving [x]
 - Introduce the proofmode hypotheses [Hs]
-*)
+
+The argument [IH] in the tactics below is either [Some "IH"], in which case
+the induction hypotheses are named "IH", "IH1", "IH2" (used for the legacy
+syntax), or [None], in which case the names from the Coq introduction pattern
+are used (they are converted from idents into strings). *)
 Tactic Notation "iInductionCore" tactic3(tac) "as" constr(IH) :=
   let rec fix_ihs rev_tac :=
     lazymatch goal with
@@ -1746,11 +1750,19 @@ Tactic Notation "iInductionCore" tactic3(tac) "as" constr(IH) :=
           fail "iInduction: spatial context not empty, this should not happen"
          |clear H];
        fix_ihs ltac:(fun j =>
-         let IH' := eval vm_compute in
-           match j with 0%N => IH | _ => IH +:+ pretty j end in
-         iIntros [IIntuitionistic (IIdent IH')];
-         let j := eval vm_compute in (1 + j)%N in
-         rev_tac j)
+         (* Written in CPS style because [ident_to_string_cps] is CPS. *)
+         let cont IH' :=
+           iIntros [IIntuitionistic (IIdent IH')];
+           let j := eval vm_compute in (1 + j)%N in
+           rev_tac j in
+         match IH with
+         | Some ?IH =>
+            let IH' := eval vm_compute in
+              match j with 0%N => IH | _ => IH +:+ pretty j end in
+            cont IH'
+         | None =>
+            ident_to_string_cps ident:(H) cont
+         end)
     | _ => rev_tac 0%N
     end in
   tac ();
@@ -1785,33 +1797,60 @@ Ltac _iInduction0 x Hs tac IH :=
   with_ltac1_nil ltac:(fun xs => _iInduction x xs Hs tac IH).
 
 (* Without induction scheme *)
+(* legacy syntax *)
 Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH) :=
-  _iInduction0 x "" ltac:(fun _ => induction x as pat) IH.
+  _iInduction0 x "" ltac:(fun _ => induction x as pat) (Some IH).
 Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
     "forall" "(" ne_ident_list(xs) ")" :=
-  _iInduction x xs "" ltac:(fun _ => induction x as pat) IH.
-
+  _iInduction x xs "" ltac:(fun _ => induction x as pat) (Some IH).
 Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
     "forall" constr(Hs) :=
-  _iInduction0 x Hs ltac:(fun _ => induction x as pat) IH.
+  _iInduction0 x Hs ltac:(fun _ => induction x as pat) (Some IH).
 Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
     "forall" "(" ne_ident_list(xs) ")" constr(Hs) :=
-  _iInduction x xs Hs ltac:(fun _ => induction x as pat) IH.
+  _iInduction x xs Hs ltac:(fun _ => induction x as pat) (Some IH).
+
+(* new syntax that uses IH names from Coq intro pattern *)
+Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) :=
+  _iInduction0 x "" ltac:(fun _ => induction x as pat) (@None string).
+Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat)
+    "forall" "(" ne_ident_list(xs) ")" :=
+  _iInduction x xs "" ltac:(fun _ => induction x as pat) (@None string).
+Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat)
+    "forall" constr(Hs) :=
+  _iInduction0 x Hs ltac:(fun _ => induction x as pat) (@None string).
+Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat)
+    "forall" "(" ne_ident_list(xs) ")" constr(Hs) :=
+  _iInduction x xs Hs ltac:(fun _ => induction x as pat) (@None string).
 
 (* With induction scheme *)
+(* legacy syntax *)
 Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
     "using" uconstr(u) :=
-  _iInduction0 x "" ltac:(fun _ => induction x as pat using u) IH.
+  _iInduction0 x "" ltac:(fun _ => induction x as pat using u) (Some IH).
 Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
     "using" uconstr(u) "forall" "(" ne_ident_list(xs) ")" :=
-  _iInduction x xs "" ltac:(fun _ => induction x as pat using u) IH.
-
+  _iInduction x xs "" ltac:(fun _ => induction x as pat using u) (Some IH).
 Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
     "using" uconstr(u) "forall" constr(Hs) :=
-  _iInduction0 x Hs ltac:(fun _ => induction x as pat using u) IH.
+  _iInduction0 x Hs ltac:(fun _ => induction x as pat using u) (Some IH).
 Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat) constr(IH)
     "using" uconstr(u) "forall" "(" ne_ident_list(xs) ")" constr(Hs) :=
-  _iInduction x xs Hs ltac:(fun _ => induction x as pat using u) IH.
+  _iInduction x xs Hs ltac:(fun _ => induction x as pat using u) (Some IH).
+
+(* new syntax that uses IH names from Coq intro pattern *)
+Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat)
+    "using" uconstr(u) :=
+  _iInduction0 x "" ltac:(fun _ => induction x as pat using u) (@None string).
+Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat)
+    "using" uconstr(u) "forall" "(" ne_ident_list(xs) ")" :=
+  _iInduction x xs "" ltac:(fun _ => induction x as pat using u) (@None string).
+Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat)
+    "using" uconstr(u) "forall" constr(Hs) :=
+  _iInduction0 x Hs ltac:(fun _ => induction x as pat using u) (@None string).
+Tactic Notation "iInduction" constr(x) "as" simple_intropattern(pat)
+    "using" uconstr(u) "forall" "(" ne_ident_list(xs) ")" constr(Hs) :=
+  _iInduction x xs Hs ltac:(fun _ => induction x as pat using u) (@None string).
 
 (** * Löb Induction *)
 Tactic Notation "iLöbCore" "as" constr (IH) :=
diff --git a/iris/proofmode/string_ident.v b/iris/proofmode/string_ident.v
index 55f8917aa4f828e96e0588fcc219104ff47cc1bf..c4a6e9479f9a8a41d6fd8bd3bd2b4f8e55fcd78b 100644
--- a/iris/proofmode/string_ident.v
+++ b/iris/proofmode/string_ident.v
@@ -1,6 +1,6 @@
 From Ltac2 Require Ltac2.
 From Coq Require Import Strings.String.
-From Coq Require Import Init.Byte.
+From Coq Require Import Init.Byte Ascii.
 From iris.prelude Require Import options.
 
 Import List.ListNotations.
@@ -12,10 +12,10 @@ Module StringToIdent.
   Ltac2 Type exn ::= [ NotStringLiteral(constr) | InvalidIdent(string) ].
 
   Ltac2 coq_byte_to_int (b : constr) : int :=
-    (match! b with
-     (* generate this line with python3 -c 'print(" ".join([\'| x%02x => %d\' % (x,x) for x in range(256)]))' *)
-     | x00 => 0 | x01 => 1 | x02 => 2 | x03 => 3 | x04 => 4 | x05 => 5 | x06 => 6 | x07 => 7 | x08 => 8 | x09 => 9 | x0a => 10 | x0b => 11 | x0c => 12 | x0d => 13 | x0e => 14 | x0f => 15 | x10 => 16 | x11 => 17 | x12 => 18 | x13 => 19 | x14 => 20 | x15 => 21 | x16 => 22 | x17 => 23 | x18 => 24 | x19 => 25 | x1a => 26 | x1b => 27 | x1c => 28 | x1d => 29 | x1e => 30 | x1f => 31 | x20 => 32 | x21 => 33 | x22 => 34 | x23 => 35 | x24 => 36 | x25 => 37 | x26 => 38 | x27 => 39 | x28 => 40 | x29 => 41 | x2a => 42 | x2b => 43 | x2c => 44 | x2d => 45 | x2e => 46 | x2f => 47 | x30 => 48 | x31 => 49 | x32 => 50 | x33 => 51 | x34 => 52 | x35 => 53 | x36 => 54 | x37 => 55 | x38 => 56 | x39 => 57 | x3a => 58 | x3b => 59 | x3c => 60 | x3d => 61 | x3e => 62 | x3f => 63 | x40 => 64 | x41 => 65 | x42 => 66 | x43 => 67 | x44 => 68 | x45 => 69 | x46 => 70 | x47 => 71 | x48 => 72 | x49 => 73 | x4a => 74 | x4b => 75 | x4c => 76 | x4d => 77 | x4e => 78 | x4f => 79 | x50 => 80 | x51 => 81 | x52 => 82 | x53 => 83 | x54 => 84 | x55 => 85 | x56 => 86 | x57 => 87 | x58 => 88 | x59 => 89 | x5a => 90 | x5b => 91 | x5c => 92 | x5d => 93 | x5e => 94 | x5f => 95 | x60 => 96 | x61 => 97 | x62 => 98 | x63 => 99 | x64 => 100 | x65 => 101 | x66 => 102 | x67 => 103 | x68 => 104 | x69 => 105 | x6a => 106 | x6b => 107 | x6c => 108 | x6d => 109 | x6e => 110 | x6f => 111 | x70 => 112 | x71 => 113 | x72 => 114 | x73 => 115 | x74 => 116 | x75 => 117 | x76 => 118 | x77 => 119 | x78 => 120 | x79 => 121 | x7a => 122 | x7b => 123 | x7c => 124 | x7d => 125 | x7e => 126 | x7f => 127 | x80 => 128 | x81 => 129 | x82 => 130 | x83 => 131 | x84 => 132 | x85 => 133 | x86 => 134 | x87 => 135 | x88 => 136 | x89 => 137 | x8a => 138 | x8b => 139 | x8c => 140 | x8d => 141 | x8e => 142 | x8f => 143 | x90 => 144 | x91 => 145 | x92 => 146 | x93 => 147 | x94 => 148 | x95 => 149 | x96 => 150 | x97 => 151 | x98 => 152 | x99 => 153 | x9a => 154 | x9b => 155 | x9c => 156 | x9d => 157 | x9e => 158 | x9f => 159 | xa0 => 160 | xa1 => 161 | xa2 => 162 | xa3 => 163 | xa4 => 164 | xa5 => 165 | xa6 => 166 | xa7 => 167 | xa8 => 168 | xa9 => 169 | xaa => 170 | xab => 171 | xac => 172 | xad => 173 | xae => 174 | xaf => 175 | xb0 => 176 | xb1 => 177 | xb2 => 178 | xb3 => 179 | xb4 => 180 | xb5 => 181 | xb6 => 182 | xb7 => 183 | xb8 => 184 | xb9 => 185 | xba => 186 | xbb => 187 | xbc => 188 | xbd => 189 | xbe => 190 | xbf => 191 | xc0 => 192 | xc1 => 193 | xc2 => 194 | xc3 => 195 | xc4 => 196 | xc5 => 197 | xc6 => 198 | xc7 => 199 | xc8 => 200 | xc9 => 201 | xca => 202 | xcb => 203 | xcc => 204 | xcd => 205 | xce => 206 | xcf => 207 | xd0 => 208 | xd1 => 209 | xd2 => 210 | xd3 => 211 | xd4 => 212 | xd5 => 213 | xd6 => 214 | xd7 => 215 | xd8 => 216 | xd9 => 217 | xda => 218 | xdb => 219 | xdc => 220 | xdd => 221 | xde => 222 | xdf => 223 | xe0 => 224 | xe1 => 225 | xe2 => 226 | xe3 => 227 | xe4 => 228 | xe5 => 229 | xe6 => 230 | xe7 => 231 | xe8 => 232 | xe9 => 233 | xea => 234 | xeb => 235 | xec => 236 | xed => 237 | xee => 238 | xef => 239 | xf0 => 240 | xf1 => 241 | xf2 => 242 | xf3 => 243 | xf4 => 244 | xf5 => 245 | xf6 => 246 | xf7 => 247 | xf8 => 248 | xf9 => 249 | xfa => 250 | xfb => 251 | xfc => 252 | xfd => 253 | xfe => 254 | xff => 255
-     end).
+    match! b with
+    (* generate this line with python3 -c 'print(" ".join([\'| x%02x => %d\' % (x,x) for x in range(256)]))' *)
+    | x00 => 0 | x01 => 1 | x02 => 2 | x03 => 3 | x04 => 4 | x05 => 5 | x06 => 6 | x07 => 7 | x08 => 8 | x09 => 9 | x0a => 10 | x0b => 11 | x0c => 12 | x0d => 13 | x0e => 14 | x0f => 15 | x10 => 16 | x11 => 17 | x12 => 18 | x13 => 19 | x14 => 20 | x15 => 21 | x16 => 22 | x17 => 23 | x18 => 24 | x19 => 25 | x1a => 26 | x1b => 27 | x1c => 28 | x1d => 29 | x1e => 30 | x1f => 31 | x20 => 32 | x21 => 33 | x22 => 34 | x23 => 35 | x24 => 36 | x25 => 37 | x26 => 38 | x27 => 39 | x28 => 40 | x29 => 41 | x2a => 42 | x2b => 43 | x2c => 44 | x2d => 45 | x2e => 46 | x2f => 47 | x30 => 48 | x31 => 49 | x32 => 50 | x33 => 51 | x34 => 52 | x35 => 53 | x36 => 54 | x37 => 55 | x38 => 56 | x39 => 57 | x3a => 58 | x3b => 59 | x3c => 60 | x3d => 61 | x3e => 62 | x3f => 63 | x40 => 64 | x41 => 65 | x42 => 66 | x43 => 67 | x44 => 68 | x45 => 69 | x46 => 70 | x47 => 71 | x48 => 72 | x49 => 73 | x4a => 74 | x4b => 75 | x4c => 76 | x4d => 77 | x4e => 78 | x4f => 79 | x50 => 80 | x51 => 81 | x52 => 82 | x53 => 83 | x54 => 84 | x55 => 85 | x56 => 86 | x57 => 87 | x58 => 88 | x59 => 89 | x5a => 90 | x5b => 91 | x5c => 92 | x5d => 93 | x5e => 94 | x5f => 95 | x60 => 96 | x61 => 97 | x62 => 98 | x63 => 99 | x64 => 100 | x65 => 101 | x66 => 102 | x67 => 103 | x68 => 104 | x69 => 105 | x6a => 106 | x6b => 107 | x6c => 108 | x6d => 109 | x6e => 110 | x6f => 111 | x70 => 112 | x71 => 113 | x72 => 114 | x73 => 115 | x74 => 116 | x75 => 117 | x76 => 118 | x77 => 119 | x78 => 120 | x79 => 121 | x7a => 122 | x7b => 123 | x7c => 124 | x7d => 125 | x7e => 126 | x7f => 127 | x80 => 128 | x81 => 129 | x82 => 130 | x83 => 131 | x84 => 132 | x85 => 133 | x86 => 134 | x87 => 135 | x88 => 136 | x89 => 137 | x8a => 138 | x8b => 139 | x8c => 140 | x8d => 141 | x8e => 142 | x8f => 143 | x90 => 144 | x91 => 145 | x92 => 146 | x93 => 147 | x94 => 148 | x95 => 149 | x96 => 150 | x97 => 151 | x98 => 152 | x99 => 153 | x9a => 154 | x9b => 155 | x9c => 156 | x9d => 157 | x9e => 158 | x9f => 159 | xa0 => 160 | xa1 => 161 | xa2 => 162 | xa3 => 163 | xa4 => 164 | xa5 => 165 | xa6 => 166 | xa7 => 167 | xa8 => 168 | xa9 => 169 | xaa => 170 | xab => 171 | xac => 172 | xad => 173 | xae => 174 | xaf => 175 | xb0 => 176 | xb1 => 177 | xb2 => 178 | xb3 => 179 | xb4 => 180 | xb5 => 181 | xb6 => 182 | xb7 => 183 | xb8 => 184 | xb9 => 185 | xba => 186 | xbb => 187 | xbc => 188 | xbd => 189 | xbe => 190 | xbf => 191 | xc0 => 192 | xc1 => 193 | xc2 => 194 | xc3 => 195 | xc4 => 196 | xc5 => 197 | xc6 => 198 | xc7 => 199 | xc8 => 200 | xc9 => 201 | xca => 202 | xcb => 203 | xcc => 204 | xcd => 205 | xce => 206 | xcf => 207 | xd0 => 208 | xd1 => 209 | xd2 => 210 | xd3 => 211 | xd4 => 212 | xd5 => 213 | xd6 => 214 | xd7 => 215 | xd8 => 216 | xd9 => 217 | xda => 218 | xdb => 219 | xdc => 220 | xdd => 221 | xde => 222 | xdf => 223 | xe0 => 224 | xe1 => 225 | xe2 => 226 | xe3 => 227 | xe4 => 228 | xe5 => 229 | xe6 => 230 | xe7 => 231 | xe8 => 232 | xe9 => 233 | xea => 234 | xeb => 235 | xec => 236 | xed => 237 | xee => 238 | xef => 239 | xf0 => 240 | xf1 => 241 | xf2 => 242 | xf3 => 243 | xf4 => 244 | xf5 => 245 | xf6 => 246 | xf7 => 247 | xf8 => 248 | xf9 => 249 | xfa => 250 | xfb => 251 | xfc => 252 | xfd => 253 | xfe => 254 | xff => 255
+    end.
 
   Ltac2 coq_byte_to_char (b : constr) : char :=
     Char.of_int (coq_byte_to_int b).
@@ -39,7 +39,7 @@ Module StringToIdent.
     match! s with
     | EmptyString => 0
     | String _ ?s' => Int.add 1 (coq_string_length s')
-    | _ => Control.throw (NotStringLiteral(s))
+    | _ => Control.throw (NotStringLiteral s)
     end.
 
   Ltac2 compute (c : constr) : constr :=
@@ -54,7 +54,7 @@ Module StringToIdent.
     let _ := coq_byte_list_blit_list 0 bytes str in
     str.
 
-  Ltac2 ident_from_string (s : string) : ident :=
+  Ltac2 string_to_ident (s : string) : ident :=
     match Ident.of_string s with
     | Some id => id
     | None => Control.throw (InvalidIdent s)
@@ -62,7 +62,7 @@ Module StringToIdent.
 
   (** [coq_string_to_ident] implements the ident to string conversion in Ltac2 *)
   Ltac2 coq_string_to_ident (s : constr) : ident :=
-    ident_from_string (coq_string_to_string s).
+    string_to_ident (coq_string_to_string s).
 
   (** We want to wrap [coq_string_to_ident] in an Ltac1 API, but Ltac1-2 FFI
   does not support returning values from Ltac2 to Ltac1. So we provide
@@ -74,10 +74,44 @@ Module StringToIdent.
                    Ltac1.apply r [Ltac1.of_ident ident] Ltac1.run).
 End StringToIdent.
 
+Module IdentToString.
+  Import Ltac2.
+
+  Ltac2 get_bit (n : int) (i : int) : bool :=
+    Int.equal (Int.land (Int.lsr n i) 1) 1.
+
+  Ltac2 get_bit_coq_bool (n : int) (i : int) : constr :=
+    if get_bit n i then constr:(true) else constr:(false).
+
+  Ltac2 char_to_coq_ascii (c : char) : constr :=
+    let i := Char.to_int c in
+    let bs := Array.init 8 (get_bit_coq_bool i) in
+    Constr.Unsafe.make (Constr.Unsafe.App constr:(Ascii) bs).
+
+  Ltac2 string_to_coq_string (s : string) : constr :=
+    let len := String.length s in
+    let rec to_string i :=
+      if Int.equal i len then constr:(EmptyString) else
+        let tail := to_string (Int.add i 1) in
+        let head := char_to_coq_ascii (String.get s i) in
+        constr:(String $head $tail)
+    in
+    to_string 0.
+
+  Ltac2 ident_to_string (id : ident) : constr :=
+    string_to_coq_string (Ident.to_string id).
+
+  Ltac ident_to_string_cps :=
+    ltac2:(id r |- let id := Option.get (Ltac1.to_ident id) in
+                   let s := ident_to_string id in
+                   Ltac1.apply r [Ltac1.of_constr s] Ltac1.run).
+End IdentToString.
+
 (** Finally we wrap everything up intro a tactic that renames a variable given
 by ident [id] into the name given by string [s]. *)
 Ltac rename_by_string id s :=
   StringToIdent.string_to_ident_cps s ltac:(fun x => rename id into x).
 
-(* We also directly expose the CPS primitive. *)
+(* We also directly expose the CPS primitives. *)
 Ltac string_to_ident_cps := StringToIdent.string_to_ident_cps.
+Ltac ident_to_string_cps := IdentToString.ident_to_string_cps.
diff --git a/iris_heap_lang/derived_laws.v b/iris_heap_lang/derived_laws.v
index a57ce3d1c7a0c834be5d79eba9850b07df639bd0..8f1552a1dc876d4ce6fbb2ca1cc49993fc5fb5c8 100644
--- a/iris_heap_lang/derived_laws.v
+++ b/iris_heap_lang/derived_laws.v
@@ -96,7 +96,7 @@ Lemma pointsto_seq_array l dq v n :
   ([∗ list] i ∈ seq 0 n, (l +ₗ (i : nat)) ↦{dq} v) -∗
   l ↦∗{dq} replicate n v.
 Proof.
-  rewrite /array. iInduction n as [|n'] "IH" forall (l); simpl.
+  rewrite /array. iInduction n as [|n' IH] forall (l); simpl.
   { done. }
   iIntros "[$ Hl]". rewrite -fmap_S_seq big_sepL_fmap.
   setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
diff --git a/iris_heap_lang/lib/array.v b/iris_heap_lang/lib/array.v
index 8ed608ab856fa0ae33032411ca7a268471dd74c1..99bc6503468959f75b9c9a10df04f2b713e6a3d1 100644
--- a/iris_heap_lang/lib/array.v
+++ b/iris_heap_lang/lib/array.v
@@ -57,7 +57,7 @@ Section proof.
     [[{ l ↦∗ vs }]] array_free #l #n @ s; E [[{ RET #(); True }]].
   Proof.
     iIntros (Hlen Φ) "Hl HΦ".
-    iInduction vs as [|v vs] "IH" forall (l n Hlen); subst n; wp_rec; wp_pures.
+    iInduction vs as [|v vs IH] forall (l n Hlen); subst n; wp_rec; wp_pures.
     { iApply "HΦ". done. }
     iDestruct (array_cons with "Hl") as "[Hv Hl]".
     wp_free. wp_pures. iApply ("IH" with "[] Hl"); eauto with lia.
@@ -77,7 +77,7 @@ Section proof.
     [[{ RET #(); dst ↦∗ vsrc ∗ src ↦∗{dq} vsrc }]].
   Proof.
     iIntros (Hvdst Hvsrc Φ) "[Hdst Hsrc] HΦ".
-    iInduction vdst as [|v1 vdst] "IH" forall (n dst src vsrc Hvdst Hvsrc);
+    iInduction vdst as [|v1 vdst IH] forall (n dst src vsrc Hvdst Hvsrc);
       destruct vsrc as [|v2 vsrc]; simplify_eq/=; try lia; wp_rec; wp_pures.
     { iApply "HΦ". auto with iFrame. }
     iDestruct (array_cons with "Hdst") as "[Hv1 Hdst]".
@@ -139,7 +139,7 @@ Section proof.
       }}}.
     Proof.
       iIntros (Hn Φ) "[Hl Hf] HΦ".
-      iInduction k as [|k] "IH" forall (i Hn); simplify_eq/=; wp_rec; wp_pures.
+      iInduction k as [|k IH] forall (i Hn); simplify_eq/=; wp_rec; wp_pures.
       { rewrite bool_decide_eq_true_2; last (repeat f_equal; lia).
         wp_pures. iApply ("HΦ" $! []). auto. }
       rewrite bool_decide_eq_false_2; last naive_solver lia.
@@ -166,7 +166,7 @@ Section proof.
       }]].
     Proof.
       iIntros (Hn Φ) "[Hl Hf] HΦ".
-      iInduction k as [|k] "IH" forall (i Hn); simplify_eq/=; wp_rec; wp_pures.
+      iInduction k as [|k IH] forall (i Hn); simplify_eq/=; wp_rec; wp_pures.
       { rewrite bool_decide_eq_true_2; last (repeat f_equal; lia).
         wp_pures. iApply ("HΦ" $! []). auto. }
       rewrite bool_decide_eq_false_2; last naive_solver lia.
@@ -232,7 +232,7 @@ Section proof.
       ([∗ list] k↦v ∈ vs, ∃ x, ⌜v = g x⌝ ∗ Q k x) -∗
       ∃ xs, ⌜ vs = g <$> xs ⌝ ∗ [∗ list] k↦x ∈ xs, Q k x.
     Proof.
-      iIntros "Hvs". iInduction vs as [|v vs] "IH" forall (Q); simpl.
+      iIntros "Hvs". iInduction vs as [|v vs IH] forall (Q); simpl.
       { iExists []. by auto. }
       iDestruct "Hvs" as "[(%x & -> & Hv) Hvs]".
       iDestruct ("IH" with "Hvs") as (xs ->) "Hxs".
diff --git a/iris_heap_lang/primitive_laws.v b/iris_heap_lang/primitive_laws.v
index 522bc118c5b271a4cdc2ddbc09d1b0e88fada573..7ba12c508c5577859865f6ff0e06f7e6a0426553 100644
--- a/iris_heap_lang/primitive_laws.v
+++ b/iris_heap_lang/primitive_laws.v
@@ -360,7 +360,7 @@ Lemma heap_array_to_seq_meta l vs (n : nat) :
   ([∗ map] l' ↦ _ ∈ heap_array l vs, meta_token l' ⊤) -∗
   [∗ list] i ∈ seq 0 n, meta_token (l +ₗ (i : nat)) ⊤.
 Proof.
-  iIntros (<-) "Hvs". iInduction vs as [|v vs] "IH" forall (l)=> //=.
+  iIntros (<-) "Hvs". iInduction vs as [|v vs IH] forall (l)=> //=.
   rewrite big_opM_union; last first.
   { apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
     intros (j&w&?&Hjl&?&?)%heap_array_lookup.
@@ -375,7 +375,7 @@ Lemma heap_array_to_seq_pointsto l v (n : nat) :
   ([∗ map] l' ↦ ov ∈ heap_array l (replicate n v), gen_heap.pointsto l' (DfracOwn 1) ov) -∗
   [∗ list] i ∈ seq 0 n, (l +ₗ (i : nat)) ↦ v.
 Proof.
-  iIntros "Hvs". iInduction n as [|n] "IH" forall (l); simpl.
+  iIntros "Hvs". iInduction n as [|n IH] forall (l); simpl.
   { done. }
   rewrite big_opM_union; last first.
   { apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index b8d209d82bcfd5281b264cff7988880445a40b64..7271517ac1939fb2a395d3f3fbc14645de01cea0 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -106,7 +106,7 @@ Section tests.
     Φ #(n2 - 1) -∗ WP FindPred #n2 #n1 @ E [{ Φ }].
   Proof.
     iIntros (Hn) "HΦ".
-    iInduction (Z.gt_wf n2 n1) as [n1' _] "IH" forall (Hn).
+    iInduction (Z.gt_wf n2 n1) as [n1' _ IH] forall (Hn).
     wp_rec. wp_pures. case_bool_decide; wp_if.
     - iApply ("IH" with "[%] [%] HΦ"); lia.
     - by assert (n1' = n2 - 1)%Z as -> by lia.
@@ -133,12 +133,12 @@ Section tests.
   side-condition of the [=] operator. *)
   Lemma Id_wp (n : nat) : ⊢ WP Id #n {{ v, ⌜ v = #() ⌝ }}.
   Proof.
-    iInduction n as [|n] "IH"; wp_rec; wp_pures; first done.
+    iInduction n as [|n IH]; wp_rec; wp_pures; first done.
     by replace (S n - 1)%Z with (n:Z) by lia.
   Qed.
   Lemma Id_twp (n : nat) : ⊢ WP Id #n [{ v, ⌜ v = #() ⌝ }].
   Proof.
-    iInduction n as [|n] "IH"; wp_rec; wp_pures; first done.
+    iInduction n as [|n IH]; wp_rec; wp_pures; first done.
     by replace (S n - 1)%Z with (n:Z) by lia.
   Qed.
 
diff --git a/tests/list_reverse.v b/tests/list_reverse.v
index 4f98fa49048928f410a04ae435eb560ac6000fec..c3f3abe87250f4e0e598e29f5b891c0d42d3af5c 100644
--- a/tests/list_reverse.v
+++ b/tests/list_reverse.v
@@ -34,7 +34,7 @@ Lemma rev_acc_wp hd acc xs ys :
   [[{ w, RET w; is_list w (reverse xs ++ ys) }]].
 Proof.
   iIntros (Φ) "[Hxs Hys] HΦ". Show.
-  iInduction xs as [|x xs] "IH" forall (hd acc ys Φ);
+  iInduction xs as [|x xs IH] forall (hd acc ys Φ);
     iSimplifyEq; wp_rec; wp_let.
   - Show. wp_match. by iApply "HΦ".
   - iDestruct "Hxs" as (l hd' ->) "[Hx Hxs]".
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index fb7915240669ea1798f5579fca414ab3db4556dd..58da080bdfedd4f0d1fc38a5407f1ee5144fdaaf 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -436,15 +436,29 @@ Tactic failure: iCombine: cannot find 'gives' clause for hypotheses
 1 goal
   
   PROP : bi
-  l, t1 : tree
+  l, r : tree
   Φ : tree → PROP
   ============================
   "Hleaf" : Φ leaf
-  "Hnode" : ∀ l0 r : tree, Φ l0 -∗ Φ r -∗ Φ (node l0 r)
+  "Hnode" : ∀ l0 r0 : tree, Φ l0 -∗ Φ r0 -∗ Φ (node l0 r0)
+  "IHl" : Φ l
+  "IHr" : Φ r
+  --------------------------------------â–¡
+  Φ (node l r)
+"test_iInduction_multiple_IHs_legacy"
+     : string
+1 goal
+  
+  PROP : bi
+  l, r : tree
+  Φ : tree → PROP
+  ============================
+  "Hleaf" : Φ leaf
+  "Hnode" : ∀ l0 r0 : tree, Φ l0 -∗ Φ r0 -∗ Φ (node l0 r0)
   "IH" : Φ l
-  "IH1" : Φ t1
+  "IH1" : Φ r
   --------------------------------------â–¡
-  Φ (node l t1)
+  Φ (node l r)
 The command has indeed failed with message:
 Tactic failure: iSpecialize: cannot instantiate (∀ _ : φ, P -∗ False)%I with
 P.
@@ -1164,6 +1178,16 @@ The command has indeed failed with message:
 Tactic failure: sel_pat.parse: the term m
 is expected to be a selection pattern (usually a string),
 but has unexpected type nat.
+"iInduction_non_fresh_IH"
+     : string
+The command has indeed failed with message:
+Tactic failure: iIntro: "IH" not fresh.
+The command has indeed failed with message:
+Tactic failure: iIntro: "IH" not fresh.
+"iInduction_non_fresh_Coq_IH"
+     : string
+The command has indeed failed with message:
+IH is already used.
 "test_iIntros_let_entails_fail"
      : string
 The command has indeed failed with message:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index c19cac183244182f61f3109a79dbd3fc0c8d4c70..4d6ba28dbc18214925781da990ee7655feece151 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -989,14 +989,14 @@ Lemma test_iInduction_wf (x : nat) P Q :
   □ P -∗ Q -∗ ⌜ (x + 0 = x)%nat ⌝.
 Proof.
   iIntros "#HP HQ".
-  iInduction (lt_wf x) as [[|x] _] "IH"; simpl; first done.
+  iInduction (lt_wf x) as [[|x] _ IH]; simpl; first done.
   rewrite (inj_iff S). by iApply ("IH" with "[%]"); first lia.
 Qed.
 
 Lemma test_iInduction_using (m : gmap nat nat) (Φ : nat → nat → PROP) y :
   ([∗ map] x ↦ i ∈ m, Φ y x) -∗ ([∗ map] x ↦ i ∈ m, emp ∗ Φ y x).
 Proof.
-  iIntros "Hm". iInduction m as [|i x m] "IH" using map_ind forall(y).
+  iIntros "Hm". iInduction m as [|i x m ? IH] using map_ind forall (y).
   - by rewrite !big_sepM_empty.
   - rewrite !big_sepM_insert //. iDestruct "Hm" as "[$ ?]".
     by iApply "IH".
@@ -1010,7 +1010,7 @@ Lemma test_iInduction_big_sepL_impl' {A} (Φ Ψ : nat → A → PROP) (l1 l2 : l
   [∗ list] k↦x ∈ l2, Ψ k x.
 Proof.
   iIntros (Hlen) "Hl #Himpl".
-  iInduction l1 as [|x1 l1] "IH" forall (Φ Ψ l2 Hlen).
+  iInduction l1 as [|x1 l1 IH] forall (Φ Ψ l2 Hlen).
 Abort.
 
 Inductive tree := leaf | node (l r: tree).
@@ -1019,7 +1019,45 @@ Check "test_iInduction_multiple_IHs".
 Lemma test_iInduction_multiple_IHs (t: tree) (Φ : tree → PROP) :
   □ Φ leaf -∗ □ (∀ l r, Φ l -∗ Φ r -∗ Φ (node l r)) -∗ Φ t.
 Proof.
-  iIntros "#Hleaf #Hnode". iInduction t as [|l r] "IH".
+  iIntros "#Hleaf #Hnode". iInduction t as [|l IHl r IHr].
+  - iExact "Hleaf".
+  - Show. (* should have "IHl" and "IHr", since [node] has two trees *)
+    iApply ("Hnode" with "IHl IHr").
+Qed.
+
+(* Copies of the above tests for the legacy syntax of naming IHs *)
+Lemma test_iInduction_wf_legacy (x : nat) P Q :
+  □ P -∗ Q -∗ ⌜ (x + 0 = x)%nat ⌝.
+Proof.
+  iIntros "#HP HQ".
+  iInduction (lt_wf x) as [[|x] _] "IH"; simpl; first done.
+  rewrite (inj_iff S). by iApply ("IH" with "[%]"); first lia.
+Qed.
+
+Lemma test_iInduction_using_legacy (m : gmap nat nat) (Φ : nat → nat → PROP) y :
+  ([∗ map] x ↦ i ∈ m, Φ y x) -∗ ([∗ map] x ↦ i ∈ m, emp ∗ Φ y x).
+Proof.
+  iIntros "Hm". iInduction m as [|i x m ?] "IH" using map_ind forall (y).
+  - by rewrite !big_sepM_empty.
+  - rewrite !big_sepM_insert //. iDestruct "Hm" as "[$ ?]".
+    by iApply "IH".
+Qed.
+
+Lemma test_iInduction_big_sepL_impl' {A} (Φ Ψ : nat → A → PROP) (l1 l2 : list A) :
+  length l1 = length l2 →
+  ([∗ list] k↦x ∈ l1, Φ k x) -∗
+  □ (∀ k x1 x2, ⌜l1 !! k = Some x1⌝ -∗ ⌜l2 !! k = Some x2⌝ -∗ Φ k x1 -∗ Ψ k x2) -∗
+  [∗ list] k↦x ∈ l2, Ψ k x.
+Proof.
+  iIntros (Hlen) "Hl #Himpl".
+  iInduction l1 as [|x1 l1] "IH" forall (Φ Ψ l2 Hlen).
+Abort.
+
+Check "test_iInduction_multiple_IHs_legacy".
+Lemma test_iInduction_multiple_IHs_legacy (t: tree) (Φ : tree → PROP) :
+  □ Φ leaf -∗ □ (∀ l r, Φ l -∗ Φ r -∗ Φ (node l r)) -∗ Φ t.
+Proof.
+  iIntros "#Hleaf #Hnode". iInduction t as [|l ? r] "IH".
   - iExact "Hleaf".
   - Show. (* should have "IH" and "IH1", since [node] has two trees *)
     iApply ("Hnode" with "IH IH1").
@@ -1619,11 +1657,11 @@ Lemma test_iInduction_revert_pure (n : nat) (Hn : 0 < n) (P : nat → PROP) :
   ⊢ P n.
 Proof.
   (* Check that we consistently get [<affine> _ -∗], not [→] *)
-  iInduction n as [|n] "IH" forall (Hn); first lia.
+  iInduction n as [|n IH] forall (Hn); first lia.
   Show.
 Restart.
 Proof.
-  iInduction n as [|n] "IH"; first lia.
+  iInduction n as [|n IH]; first lia.
   Show.
 Abort.
 
@@ -1632,11 +1670,11 @@ Lemma test_iInduction_revert_pure_affine `{!BiAffine PROP}
   (n : nat) (Hn : 0 < n) (P : nat → PROP) : ⊢ P n.
 Proof.
   (* Check that we consistently get [-∗], not [→]; and no [<affine>] *)
-  iInduction n as [|n] "IH" forall (Hn); first lia.
+  iInduction n as [|n IH] forall (Hn); first lia.
   Show.
 Restart.
 Proof.
-  iInduction n as [|n] "IH"; first lia.
+  iInduction n as [|n IH]; first lia.
   Show.
 Abort.
 
@@ -2054,7 +2092,27 @@ Check "iInduction_wrong_sel_pat".
 Lemma iInduction_wrong_sel_pat (n m : nat) (P Q : nat → PROP) :
   ⌜ n = m ⌝ -∗ P n -∗ P m.
 Proof.
-  Fail iInduction n as [|n] "IH" forall m.
+  Fail iInduction n as [|n IH] forall m.
+Abort.
+
+Check "iInduction_non_fresh_IH".
+Lemma iInduction_non_fresh_IH Q (P : nat → PROP) n :
+  □ Q -∗ P n.
+Proof.
+  iIntros "IH".
+  Fail iInduction n as [|n IH].
+  Fail iInduction n as [|n] "IH".
+Abort.
+
+Check "iInduction_non_fresh_Coq_IH".
+Lemma iInduction_non_fresh_Coq_IH φ (P : nat → PROP) n :
+  □ ⌜ φ ⌝ -∗ P n.
+Proof.
+  iIntros (IH).
+  (* Names for IHs should also be fresh in Coq context *)
+  Fail iInduction n as [|n IH].
+  (* But for the legacy syntax this is no problem. *)
+  iInduction n as [|n] "IH".
 Abort.
 
 Check "test_iIntros_let_entails_fail".
@@ -2287,7 +2345,7 @@ Section mutual_induction.
     □ (∀ l, (∀ x, ⌜ x ∈ l ⌝ → P x) -∗ P (Tree l)) -∗
     ∀ t, P t.
   Proof.
-    iIntros "#H" (t). iInduction t as [] "IH".
+    iIntros "#H" (t). iInduction t as [l IH].
     Show. (* make sure that the induction hypothesis is exactly what we want *)
     iApply "H". iIntros (x ?). by iApply (big_sepL_elem_of with "IH").
   Qed.
@@ -2314,7 +2372,7 @@ Section mutual_induction.
     ∀ t, P t.
   Proof.
     iIntros "#H" (t).
-    Fail iInduction t as [] "IH" using ntree_ind_alt.
+    Fail iInduction t as [l IH] using ntree_ind_alt.
   Abort.
 End mutual_induction.
 
diff --git a/tests/tree_sum.v b/tests/tree_sum.v
index b5683256d0d2dd0652c28a8dbca44e129abc4038..c151d1ecfb8ee38339fbf81b4bfe4b4f7623cfcb 100644
--- a/tests/tree_sum.v
+++ b/tests/tree_sum.v
@@ -40,13 +40,13 @@ Lemma sum_loop_wp `{!heapGS Σ} v t l (n : Z) :
   [[{ RET #(); l ↦ #(sum t + n) ∗ is_tree v t }]].
 Proof.
   iIntros (Φ) "[Hl Ht] HΦ".
-  iInduction t as [n'|tl ? tr] "IH" forall (v l n Φ); simpl; wp_rec; wp_let.
+  iInduction t as [n'|tl IHl tr IHr] forall (v l n Φ); simpl; wp_rec; wp_let.
   - iDestruct "Ht" as "%"; subst.
     wp_load. wp_store.
     by iApply ("HΦ" with "[$Hl]").
   - iDestruct "Ht" as (ll lr vl vr ->) "(Hll & Htl & Hlr & Htr)".
-    wp_load. wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]".
-    wp_load. wp_apply ("IH1" with "Hl Htr"). iIntros "[Hl Htr]".
+    wp_load. wp_apply ("IHl" with "Hl Htl"). iIntros "[Hl Htl]".
+    wp_load. wp_apply ("IHr" with "Hl Htr"). iIntros "[Hl Htr]".
     iApply "HΦ". iSplitL "Hl".
     { by replace (sum tl + sum tr + n)%Z with (sum tr + (sum tl + n))%Z by lia. }
     iExists ll, lr, vl, vr. by iFrame.