aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.ml
diff options
context:
space:
mode:
authorJoachim Breitner2018-10-01 22:09:33 -0700
committerJoachim Breitner2018-10-01 22:09:33 -0700
commit2d31d956fb708add948d0126b7c616375abf6358 (patch)
treee9dbebc3c0d4d8e203eebdb14f394e68fd39de62 /kernel/type_errors.ml
parent05786b23cf0d031c93998c59f6f2f94d6049b027 (diff)
Docs: Missing backquote
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions