diff options
| author | Enrico Tassi | 2019-03-28 09:52:06 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-03-28 09:52:17 +0100 |
| commit | 6d0ffe795f6f29730d59c379285201fd46023935 (patch) | |
| tree | a0e31f24ce950f79fe7fdae5a4dddc5101cb91fa /kernel/type_errors.ml | |
| parent | 383bcf46b12799762fefec7e06fe00b5e33f5a18 (diff) | |
| parent | 7637dc2dd51dd336249cefa828ec95790b3c88c5 (diff) | |
Merge PR #9743: Relax the ambiguous path condition of coercion
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: gares
Ack-by: pi8027
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions