diff options
| author | Gaëtan Gilbert | 2018-06-21 15:07:56 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-07-12 14:07:25 +0200 |
| commit | cb219011534a8de24a01ddb007799133cdd2cb0e (patch) | |
| tree | e754dd9853ef891c5daecfa6987881048f8952b1 /dev/ci | |
| parent | 31fce698ec8c3186dc6af49961e8572e81cab50b (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 'dev/ci')
0 files changed, 0 insertions, 0 deletions
