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 /pretyping/typeclasses_errors.mli | |
| 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 'pretyping/typeclasses_errors.mli')
0 files changed, 0 insertions, 0 deletions