aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.mli
diff options
context:
space:
mode:
authorMatej Kosik2017-02-03 09:02:41 +0100
committerMatej Košík2017-04-10 13:16:58 +0200
commit9b627431516f2cf88312329def9e0ec5e8605a98 (patch)
tree8ffb803784d3be7abd274151596cce81477d90a6 /kernel/type_errors.mli
parent28973285f4b9389ed0610b94ba907684214dd279 (diff)
trivial
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions