diff options
| author | Théo Zimmermann | 2018-09-07 19:17:32 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-07 19:17:32 +0200 |
| commit | 69fb545f0fad2b356f5be1ce3e1a24b5afe26ce2 (patch) | |
| tree | 35992039843accc4b8074cc15f9720589d1df38b /kernel/type_errors.mli | |
| parent | de08e8bfcaa000b4dcee33f5bb10b17039727709 (diff) | |
| parent | 6d85d5e825f19f3e2103273648d8c7976d115ec9 (diff) | |
Merge PR #8437: Recover lost snippet
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions