diff options
| author | Emilio Jesus Gallego Arias | 2019-06-26 01:12:16 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-26 01:12:16 +0200 |
| commit | 7e0697d6931d250fec2b1ff5092148d8ea11c4d3 (patch) | |
| tree | a5733301e8a031fbe7a53a0b40ffdcddaff38bab /kernel/type_errors.ml | |
| parent | b77084ebafe8ed2a8a4002b574078f592274a89c (diff) | |
| parent | 8948a2066c7172537a48f49987a79e6bfaab899c (diff) | |
Merge PR #10427: Move internal flag
Reviewed-by: ejgallego
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions