diff options
| author |  mlasson <marc.lasson@gmail.com> | 2015-06-25 19:50:15 +0200 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2015-09-03 00:47:37 +0200 |
| commit | 60b5e9c05e0c168e30eafede545c221e63d12ea2 (patch) | |
| tree | 3691a6b1a108157eaf6a8eb79f192f1f23d8675a /checker/indtypes.ml | |
| parent | 518049fe7f689489842fdfa670f57b618f125f31 (diff) | |
Also there's an extra space in the error message.
Diffstat (limited to 'checker/indtypes.ml')
0 files changed, 0 insertions, 0 deletions