| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5. |  Pierre-Marie Pédrot | 2015-11-19 |
| 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. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |