diff options
| author | Hugo Herbelin | 2017-11-05 12:21:36 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-05 12:31:04 +0100 |
| commit | 6304c843c01cd1cb4fcd940d74f6ddb414cb6914 (patch) | |
| tree | c9db2f22565e952bdf3ab6739b5bc42cc39d81a6 /dev/db | |
| parent | f281a8a88e8fc7c41cc5680db2443d9da33b47b7 (diff) | |
Refining PR#924 (insensitivity of projection heuristics to alphabet).
We refine the criterion for selecting a projection. Before PR#924 it
was alphabetic (i.e. morally "random" up to alpha-conversion). After
PR#924 it was chronological.
We refine a bit more by giving priority to simple projections when
they exist over projections which include an evar instantiation (and
which may actually be ill-typed).
Diffstat (limited to 'dev/db')
0 files changed, 0 insertions, 0 deletions