diff options
| author | Clément Pit-Claudel | 2019-03-07 09:28:30 -0500 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-03-07 09:28:30 -0500 |
| commit | 29b85080afef1c83ee772de3e69c487627ae6ce5 (patch) | |
| tree | 1a9517a8c885a81587eae6eb9acbfaba417e0089 /kernel/type_errors.ml | |
| parent | c9fd99644e223ada3aad53915f1cd0d2598882b3 (diff) | |
| parent | 52b29f236ee2535257df1439740e5c86ed17e69d (diff) | |
Merge PR #9133: Move README-V1-V5 to credits chapter
Reviewed-by: cpitclaudel
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions