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.
---
 test-suite/bugs/closed/bug_9494.v | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_9494.v

(limited to 'test-suite')

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