From e5890700b4574ee9207b2daf6ec95707b9290275 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 31 Aug 2020 12:54:54 +0200
Subject: Fix mangle names issue in induction

Fix #12944
---
 tactics/tactics.ml                 |  2 +-
 test-suite/bugs/closed/bug_12944.v | 12 ++++++++++++
 2 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/bug_12944.v

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 00bd56d8ba..28e841d4ae 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3317,7 +3317,7 @@ let induct_discharge with_evars dests avoid' tac (avoid,ra) names =
         Proofview.Goal.enter begin fun gl ->
         let (recpat,names) = match names with
           | [{CAst.loc;v=IntroNaming (IntroIdentifier id)} as pat] ->
-              let id' = next_ident_away (add_prefix "IH" id) avoid in
+              let id' = new_fresh_id avoid (add_prefix "IH" id) gl in
               (pat, [CAst.make @@ IntroNaming (IntroIdentifier id')])
           | _ -> consume_pattern avoid (Name recvarname) deprec gl names in
         let dest = get_recarg_dest dests in
diff --git a/test-suite/bugs/closed/bug_12944.v b/test-suite/bugs/closed/bug_12944.v
new file mode 100644
index 0000000000..d6720d9906
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12944.v
@@ -0,0 +1,12 @@
+
+Inductive vector A : nat -> Type :=
+  |nil : vector A 0
+  |cons : forall (h:A) (n:nat), vector A n -> vector A (S n).
+
+Global Set Mangle Names.
+
+Lemma vlookup_middle {A n} (v : vector A n) : True.
+Proof.
+  induction v as [|?? IHv].
+  all:exact I.
+Qed.
-- 
cgit v1.2.3