aboutsummaryrefslogtreecommitdiff
path: root/kernel/term.mli
diff options
context:
space:
mode:
authorMatthieu Sozeau2016-06-27 16:37:15 +0200
committerMatthieu Sozeau2016-06-27 23:13:52 +0200
commit727dcedd8d1d6be5c77cbf4bbe08ff18facf3ba2 (patch)
treeccbf21e6aa9f969210c0c4c89f18b238d132fe91 /kernel/term.mli
parent6ae5029770567b11f5872d33be63357ff3a0cb17 (diff)
Typeclasses: fix treatment of exceptions in compat
Diffstat (limited to 'kernel/term.mli')
0 files changed, 0 insertions, 0 deletions