Avoid eqn when generating name in induction_gen.

Fixes #9494.
Was failing with "Cannot create self-referring hypothesis" when
the generated name equaled the eqn.

2 files changed, 14 insertions, 1 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 070b2356e5..f41706c35e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4522,8 +4522,11 @@ let induction_gen clear_flag isrec with_evars elim
      declaring the induction argument as a new local variable *)
     let id =
     (* Type not the right one if partially applied but anyway for internal use*)
+      let avoid = match eqname with
+        | Some {CAst.v=IntroIdentifier id} -> Id.Set.singleton id
+        | _ -> Id.Set.empty in
       let x = id_of_name_using_hdchar env evd t Anonymous in
-      new_fresh_id Id.Set.empty x gl in
+      new_fresh_id avoid x gl in
     let info_arg = (is_arg_pure_hyp, not enough_applied) in
     pose_induction_arg_then
       isrec with_evars info_arg elim id arg t inhyps cls
diff --git a/test-suite/bugs/closed/bug_9494.v b/test-suite/bugs/closed/bug_9494.v
new file mode 100644
index 0000000000..a0b8383d16
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9494.v
@@ -0,0 +1,10 @@
+Lemma foo (a : nat) : True.
+Proof.
+destruct a eqn:n; exact I.
+Qed.
+
+Set Mangle Names.
+Lemma foo2 (a : nat) : True.
+Proof.
+let N := fresh in destruct a eqn:N; exact I.
+Qed.