diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-08 12:32:09 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-08 12:32:15 +0100 |
commit | 464ef8adf143b4c08252aa5148583aa52f65464c (patch) | |
tree | 68dafa21563e4155fb8a4442656c31d8fc017ee9 /kernel/subtyping.ml | |
parent | 35219fd89ce9a1b7ce92316ee84e3c8ad40b3831 (diff) |
Fixing missing separator in an error message.
The message is the "Conversion test raised an anomaly" one.
Diffstat (limited to 'kernel/subtyping.ml')
0 files changed, 0 insertions, 0 deletions