diff options
| author | Théo Zimmermann | 2020-07-17 14:38:39 +0200 |
|---|---|---|
| committer | GitHub | 2020-07-17 14:38:39 +0200 |
| commit | c3f0ebe96ad20e5c96e612f3c767b6f244dd932b (patch) | |
| tree | ef5d5f6e02dba032985ee41645ae6444e1b491f8 /kernel/type_errors.mli | |
| parent | 730f9d3aa6e89c0c20e528c07820a03950965fbb (diff) | |
Wording improvements.
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions