diff options
| author | Pierre-Marie Pédrot | 2019-02-05 15:56:36 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-05 15:56:36 +0100 |
| commit | b307529a3888ab632b7076a793904d150d263eac (patch) | |
| tree | 105892da79735e63bb59f8ae1089fabcb0adbaa0 /kernel/type_errors.ml | |
| parent | 38b1682ee6b6342ca582bac4e658f7d1c3919de4 (diff) | |
| parent | 5531d049b2a4f4c6c9e55ad31acae5b31aeda5c5 (diff) | |
Merge PR #9373: Kernel: don't automatically downgrade ill-shaped primitive records
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions