From d708030189a1c464c110706b5c239e5071a901c9 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Wed, 6 Feb 2019 13:21:51 -0800
Subject: 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.
---
 tactics/tactics.ml                |  5 ++++-
 test-suite/bugs/closed/bug_9494.v | 10 ++++++++++
 2 files changed, 14 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/bug_9494.v

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.
-- 
cgit v1.2.3