aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelib.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-06-21 15:07:56 +0200
committerGaëtan Gilbert2018-07-12 14:07:25 +0200
commitcb219011534a8de24a01ddb007799133cdd2cb0e (patch)
treee754dd9853ef891c5daecfa6987881048f8952b1 /kernel/nativelib.ml
parent31fce698ec8c3186dc6af49961e8572e81cab50b (diff)
Cleanup reduction effects: they only work on constants.
We only ever call `reduction_effect_hook` on constants, so there's no point allowing it to be declared with globrefs. There is also no point using a constr map instead of constant map. (Technically there was a call of the effect hook on projections, but that can never match a globref so it was useless)
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions