aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.mli
diff options
context:
space:
mode:
authorMatthieu Sozeau2014-06-26 13:37:30 +0200
committerMatthieu Sozeau2014-06-26 13:37:30 +0200
commit2fceedc145a0842ec4fa81f488615ea75ac9a29d (patch)
tree9bde9b00ca268566c6b497e5e6a53fa0b0b7362e /kernel/type_errors.mli
parentb443e5ce3ea09d82574b0a3196041737f0a5dcc7 (diff)
This has been fixed.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions