aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.mli
diff options
context:
space:
mode:
authorMatthieu Sozeau2014-06-26 13:54:16 +0200
committerMatthieu Sozeau2014-06-26 13:54:16 +0200
commit0b78edbafedf87f150840228f7d3b7938c809c14 (patch)
treeabc07c4c71a7d04b2b4634bb6e20b2c75cd74794 /kernel/type_errors.mli
parent2fceedc145a0842ec4fa81f488615ea75ac9a29d (diff)
Duplicate
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions