diff options
| author | Pierre-Marie Pédrot | 2020-01-13 15:16:08 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-01-13 15:16:08 +0100 |
| commit | 7cde333abd7a1c25765a9438d1b830a133a15498 (patch) | |
| tree | 3a1b4ea6e327e746c111feeb5a1bb34ff1da5c71 /kernel/nativecode.ml | |
| parent | 7d81f23fa6bd187c978b44cc6fb7218ca221fb51 (diff) | |
| parent | 8792f98500b73dd2085ad79fd14afb23a8165c4a (diff) | |
Merge PR #11285: fix #11279. Specialize h no longer expands letins in the type of h.
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions