diff options
| author | Pierre-Marie Pédrot | 2016-03-20 16:01:52 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-20 16:23:25 +0100 |
| commit | 09c2011fbdbb2ac1ce33e5abe52d93b907b21a3c (patch) | |
| tree | 7d6bba5302593d8b921f6bd174449eed227e6bb3 /engine | |
| parent | c8dcfc691a649ff6dfb3416809c6ec7b1e629b1f (diff) | |
Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4.
The interpretation of arguments of tactic notations were normalizing the goal
beforehand, which incurred an important time penalty. We now do this argumentwise
which allows to save time in frequent cases, notably tactic arguments.
Diffstat (limited to 'engine')
0 files changed, 0 insertions, 0 deletions