aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-02-13 17:49:21 +0100
committerPierre-Marie Pédrot2018-03-04 15:13:02 +0100
commit16c884413bbf2f0b5fb43bd0be7da0bf7c5e4e75 (patch)
treea0685d4245d355104d2c84feaf0950df6fb18e02 /kernel/nativelambda.mli
parentdf9d3a36e71d6d224286811fdc529ad5a955deb7 (diff)
Pass the constant cache as a separate argument in kernel reduction.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions