diff options
| author | Gaëtan Gilbert | 2020-01-08 15:05:43 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-08 15:05:43 +0100 |
| commit | b58379a9dbe1eaff122092925898ae8d51265da9 (patch) | |
| tree | 4a3aeccc5901674b3ead0d25ccc67863e69015f4 /kernel/type_errors.ml | |
| parent | cfc41cb79e2364f19d97e7e5c94262132972b0b2 (diff) | |
Close #11133
Fixed by 8750682e367d7e78634bf88e667e4c9e7c3613d3 (#9915)
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions