diff options
| author | Clément Pit-Claudel | 2018-04-30 09:53:18 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2018-05-15 12:05:44 -0400 |
| commit | a6545a120c6587af38883597d20ac28131b813a9 (patch) | |
| tree | 5e6f088e8229abd0236c94b60b8516cb24a85331 /kernel/type_errors.ml | |
| parent | dc5b6e15a2db658fb36754608683b10f847b3e94 (diff) | |
[doc] Clarify a comment in the README
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions