diff options
| author | Jasper Hugunin | 2019-02-06 13:21:51 -0800 |
|---|---|---|
| committer | Jasper Hugunin | 2019-02-06 13:21:51 -0800 |
| commit | d708030189a1c464c110706b5c239e5071a901c9 (patch) | |
| tree | 9ef02c284010207a9d2350f4570777f6814cc819 /test-suite | |
| parent | 7886c6d8e0663ba346fff52837012c7fc952ecc1 (diff) | |
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.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_9494.v | 10 |
1 files changed, 10 insertions, 0 deletions
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. |