diff options
| author | Emilio Jesus Gallego Arias | 2020-02-21 16:18:54 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-21 16:18:54 -0500 |
| commit | c45b7e41a1caa4d5ec4785c2bf323bdd11ad8d2e (patch) | |
| tree | 86d2847ee9b7c34c602fe41715afa171e41ffeba /kernel/type_errors.mli | |
| parent | 3f7eb03c82c9db9673cc8ae9c81c8f9132003751 (diff) | |
| parent | 779b8a105e3e06bde673c1abc4f918101c113fe2 (diff) | |
Merge PR #11261: Use implicit types for printing (granting wish #10366).
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions