aboutsummaryrefslogtreecommitdiff
path: root/kernel/cClosure.ml
diff options
context:
space:
mode:
authorMaxime Dénès2016-10-03 11:09:03 +0200
committerMaxime Dénès2016-10-03 11:13:40 +0200
commita35a3fd5cf59e262e814afd530ffdc35f085c01d (patch)
tree87a13102f6145c238b0696313ceb722beff09f00 /kernel/cClosure.ml
parent24d5448c65ba05072a5ab4180c9be95670ce126d (diff)
parent0746578040e738d079bcc3289857bb99983a7a22 (diff)
Merge remote-tracking branch 'github/pr/304' into v8.6
Was PR#304: fixing bug 4609
Diffstat (limited to 'kernel/cClosure.ml')
0 files changed, 0 insertions, 0 deletions