diff options
| author | Pierre-Marie Pédrot | 2017-04-08 01:42:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-04-08 02:07:26 +0200 |
| commit | 9d1230d484a2cf519f9cd76dc0f37815f3c6339b (patch) | |
| tree | cde7182712f03ea19b8151584599151818d53c0e /kernel/type_errors.ml | |
| parent | 2ba1351849550c50e0fe2c7fc7f63758c10fb14a (diff) | |
Fix a heuristic used by legacy typeclass resolution.
The evarmap used by the heuristic could contain resolved evars, which could
lead to a failure of backtracking in the EConstr branch. This is experimental
and may be to costly.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions