diff options
| author | Hugo Herbelin | 2017-08-01 21:23:35 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2017-08-02 16:47:54 +0200 |
| commit | 624c4a6b871ab4f6a02bc8e8da6862aafe3d5f73 (patch) | |
| tree | c726975f47c571ab6167abe1131554140ae2373d /kernel/type_errors.ml | |
| parent | 13dcab5b8f40058b7597e51a44207c0745eab9fd (diff) | |
Rephrasing the introduction in a more factual and up-to-date way.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions