aboutsummaryrefslogtreecommitdiff
path: root/kernel/typeops.mli
diff options
context:
space:
mode:
authorMaxime Dénès2017-07-28 18:23:36 +0200
committerMaxime Dénès2017-07-28 18:23:36 +0200
commit3828267b6dcd60088a11fe0b9613871e4fc7c54f (patch)
treeacba2a7cbfb775ce570a13f1894a6f6161d3f617 /kernel/typeops.mli
parenteaff3b36a178416f1828d75a4d46afc687953cea (diff)
parent906b48ff401f22be6059a6cdde8723b858102690 (diff)
Merge PR #888: Stronger kernel types
Diffstat (limited to 'kernel/typeops.mli')
0 files changed, 0 insertions, 0 deletions