diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-19 18:40:32 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-19 20:16:45 +0100 |
| commit | 574e510ba069f1747ecb1e5a17cf86c902d79d44 (patch) | |
| tree | 694fa60567202af7e66f71b5a9fb727d2753dc24 /library/global.ml | |
| parent | cfc0fc0075784e75783c9b4482fd3f4b858a44bf (diff) | |
Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5.
The issue was due to the fact that unfold hints are given a priority of 4
by default. As eauto was now using hint priority rather than the number of
goals produced to order the application of hints, unfold were almost always
used too late. We fixed this by manually giving them a priority of 1 in the
eauto tactic.
Also fixed the relative order of proof depth w.r.t. hint priority. It should not
be observable except for breadth-first search, which is seldom used.
Diffstat (limited to 'library/global.ml')
0 files changed, 0 insertions, 0 deletions