aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorMatthieu Sozeau2014-10-15 11:41:37 +0200
committerMatthieu Sozeau2014-10-15 11:49:00 +0200
commit707edf9b1e7310bd213678452950aaaa9e4e95f8 (patch)
treec35f38ead1b4ab5428b0cf06ecde45405874d77f /kernel
parent04ee4f9160dec2d854bd45fcff4dac08ada39b61 (diff)
Modify the heuristic for unfolding lhs or rhs in evarconv, considering
folded primitive projections in applicative stacks in rhs as named, hence prefering to unfold the lhs in these cases.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions