diff options
| author | Hugo Herbelin | 2017-07-27 00:29:51 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-07-27 11:15:09 +0200 |
| commit | c24bcae8dbc2ef82f72b3351783cbf73d3b12795 (patch) | |
| tree | f14218cc20a7967f5d01d606643479ce03477912 /dev/doc | |
| parent | bd1a0abf49fe67e7f02dc562d4b81d27ed6f606c (diff) | |
Fixing one part of #5669 (unification heuristics sensitive to choice of names).
This surprising bug was caused by an Id.Set which was ordering
solutions to variable-projection problems in ascii order.
We fix it by re-considering the variables involved in the solutions
using the declaration order.
Note that in practice, this implies preferring a dependent solution
over a non-dependent one.
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions