aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/typeops.ml
diff options
context:
space:
mode:
authorGravatar Matej Kosik <m4tej.kosik@gmail.com>2016-02-15 23:33:01 +0100
committerGravatar Matej Kosik <m4tej.kosik@gmail.com>2016-02-15 23:33:01 +0100
commit13e847b7092d53ffec63e4cba54c67d39560e67a (patch)
tree9303e5293a739b6bf77b6557da523ab4c3b171d7 /kernel/typeops.ml
parent97d6583a0b9a65080639fb02deba4200f6276ce6 (diff)
CLEANUP: Simplifying the changes done in "checker/*"
Diffstat (limited to 'kernel/typeops.ml')
0 files changed, 0 insertions, 0 deletions