diff options
author | 2014-10-01 23:27:09 +0200 | |
---|---|---|
committer | 2014-10-02 00:07:10 +0200 | |
commit | cf36105854c9a42960ee4139c6afdaa75ec8f31a (patch) | |
tree | 511a77e04d5c81167136cc5fc06233a142ba9ae2 /stm/tacworkertop.mllib | |
parent | ef0137b1782d01426938578b487052abb918d527 (diff) |
Move eta-expansion after delta reduction in kernel reduction. This makes
it closer to evarconv/unification's behavior and it is less prone
to weird failures and successes in case of first-order unification
sending problems where the two terms have different types.
Diffstat (limited to 'stm/tacworkertop.mllib')
0 files changed, 0 insertions, 0 deletions