diff options
| author | Matthieu Sozeau | 2014-10-14 18:28:58 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-10-14 18:32:35 +0200 |
| commit | ee5ea47d525530ea99203211668effc3ae3b30f8 (patch) | |
| tree | 41cfd6c840971a4001a135e6d949e304001e7706 /kernel/inductive.ml | |
| parent | 5ce9a1ab622c9b6982a42e8d5cd217787eea8745 (diff) | |
Revert "Move eta-expansion after delta reduction in kernel reduction. This makes"
This makes CatsInZFC explode by expanding constants unnecessarily.
This reverts commit cf36105854c9a42960ee4139c6afdaa75ec8f31a.
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions