diff options
| author | Pierre Courtieu | 2019-12-13 22:50:42 +0100 |
|---|---|---|
| committer | Pierre Courtieu | 2020-01-12 23:32:34 +0100 |
| commit | 8792f98500b73dd2085ad79fd14afb23a8165c4a (patch) | |
| tree | 2185f1df4e3236c78c817febcbdb5bbba509f5e1 /kernel/type_errors.ml | |
| parent | cea51c865f52841b02d64da06f04b29f893a8d4a (diff) | |
fix #11279. Specialize h no longer expands letins in the type of h.
The type of h is reconstructed to look as much as the initial type of
h as possible.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions