diff options
| author | Matthieu Sozeau | 2014-10-01 23:27:09 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-10-02 00:07:10 +0200 |
| commit | cf36105854c9a42960ee4139c6afdaa75ec8f31a (patch) | |
| tree | 511a77e04d5c81167136cc5fc06233a142ba9ae2 /lib/cArray.ml | |
| 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 'lib/cArray.ml')
0 files changed, 0 insertions, 0 deletions