aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-10 23:02:01 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-12 11:20:30 +0100
commita9efdae884ca14a180e049ef47897ec04c411247 (patch)
tree2c542f54711584a71f9e6c662dc54dcf993216ee /configure.ml
parenta1f135553d121234af0441b4dea25f5c479975c1 (diff)
Further clean-up in Reductionops, removing unused lift arguments.
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions