aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/reduction.ml
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-02-02 14:10:13 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-02-02 14:41:23 +0100
commitc9839e30e1b46e70c85533d95e4f4cc2ae826c66 (patch)
treec2b64c78b51aa85f66020d8c89e4a59888fc380f /checker/reduction.ml
parent338bac67b6c1111229d90c45875653171bbed4b3 (diff)
checker: remove unused per-constant reduction flags.
Diffstat (limited to 'checker/reduction.ml')
0 files changed, 0 insertions, 0 deletions