diff options
author | 2017-11-03 11:01:16 +0100 | |
---|---|---|
committer | 2017-11-03 11:01:16 +0100 | |
commit | f281a8a88e8fc7c41cc5680db2443d9da33b47b7 (patch) | |
tree | 2c75844e980840d2d4f25b8a27de936ae3c370f8 /pretyping/pretyping.mllib | |
parent | 96a8d73edaa4eba500c440e5d6869fae1af91a12 (diff) | |
parent | 0f66537db5df9a7f5ba9a056fd21ff34e83cc8dc (diff) |
Merge PR #6060: Improve error message and fix #6055 (spelling mistake).
Diffstat (limited to 'pretyping/pretyping.mllib')
0 files changed, 0 insertions, 0 deletions