aboutsummaryrefslogtreecommitdiff
path: root/kernel/reduction.ml
diff options
context:
space:
mode:
authorMatthieu Sozeau2014-10-14 16:30:34 +0200
committerMatthieu Sozeau2014-10-14 16:30:34 +0200
commit5ce9a1ab622c9b6982a42e8d5cd217787eea8745 (patch)
tree643354c34716c4426e347a93811a5ae38aa729b8 /kernel/reduction.ml
parenta0f3e1fe045d069cb28af21e88ea60d6b3b79c74 (diff)
Oops, forgot a fix needed after the rebase.
Diffstat (limited to 'kernel/reduction.ml')
0 files changed, 0 insertions, 0 deletions