aboutsummaryrefslogtreecommitdiff
path: root/kernel/reduction.ml
diff options
context:
space:
mode:
authorHugo Herbelin2014-10-23 20:48:38 +0200
committerHugo Herbelin2014-10-24 16:44:48 +0200
commit08e87eb96ab67ead60d92394eec6066d9b52e55e (patch)
tree9a51bbbec185b601dd38bb7682347c5025c7b08b /kernel/reduction.ml
parentf9386dc81a403e926908db7574702c0c566334e2 (diff)
Apparently, the former refine was simplifying in hypotheses too.
Diffstat (limited to 'kernel/reduction.ml')
0 files changed, 0 insertions, 0 deletions