diff options
| author | Matthieu Sozeau | 2016-05-20 03:40:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-16 18:21:08 +0200 |
| commit | b91d322b646edf753ca9f3659563e4d6c525d3f6 (patch) | |
| tree | 519fb31febe2cc6e7be6e9ac6839d6f424d3b2d4 /kernel/cbytecodes.ml | |
| parent | 2c07b6d95c7b8fd754cdf9dd767dda989723125a (diff) | |
Typeclasses: refine the eauto tactic
- Treat shelved dependent subgoals that might not be
resolved after some proof search correctly by restarting
their resolution as soon as possible (if they are
typeclasses in only_classes mode).
- Treat dependencies between goals better, avoiding
backtracking more often when dependencies allow.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions