diff options
| author | Hugo Herbelin | 2020-10-21 16:17:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-17 07:36:01 +0100 |
| commit | f1e1f8155b552e9359fe60864f46155fca28a81b (patch) | |
| tree | cdbbd36a579782bca099a210d4071c07063a808a /kernel/type_errors.ml | |
| parent | 04b25a7635e796ad05ef7db537883594a5144a56 (diff) | |
Fixes #13235: remove fragile tolerance for degenerate in-hyps clause.
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions