diff options
| author | Hugo Herbelin | 2014-12-03 13:07:35 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-03 19:24:13 +0100 |
| commit | 3b85b2bb48261ed262106e5591fa459bd3d94d73 (patch) | |
| tree | 5d0b721bce2483fc59ebb9639316a23fe2f21c07 /dev | |
| parent | e2fa65fccb9d55ea0b6bd5873155abf436785b1f (diff) | |
In solve_evar_evar, orient the heuristic over arities with different
types as it was before commit 710bae2a8c81a44.
There is still at least one problem with bug #3392 to solve.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions