diff options
| author | Guillaume Melquiond | 2015-09-18 08:00:14 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-09-18 08:00:14 +0200 |
| commit | 04e9be59051ca60bf61d5142ac14386920876926 (patch) | |
| tree | 82f783daa47f0d5e5130237b783079e1805289e0 /kernel/type_errors.ml | |
| parent | fbb3ccdb099170e5a39c9f39512b1ab2503951ea (diff) | |
Do not compress match constructs when the inner match contains no branch. (Fix bug #4348)
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions