aboutsummaryrefslogtreecommitdiff
path: root/kernel/reduction.ml
diff options
context:
space:
mode:
authorMaxime Dénès2015-10-15 14:38:57 +0200
committerMaxime Dénès2015-10-15 14:38:57 +0200
commitba8dd1c47bcbbcd2678eca78783db7f5c95f37e7 (patch)
treed7cba397b0f9e6ece420352b5dfba877e713d421 /kernel/reduction.ml
parent44817bf722eacb0379bebc7e435bfafa503d574f (diff)
Test file for #4346: Set is no longer of type Type
Diffstat (limited to 'kernel/reduction.ml')
0 files changed, 0 insertions, 0 deletions