diff options
| author | Pierre-Marie Pédrot | 2020-12-10 18:12:23 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-12 14:36:43 +0100 |
| commit | 12d53dc64fa565ae6408d2ebb668e997b7e574b3 (patch) | |
| tree | d62021097f2cd8116baedcfa98f43eef9fdc361b /tactics/redexpr.ml | |
| parent | 35ead413491cb0297dff4458d4a891cdc607b0d9 (diff) | |
Extrude the computation of redexp flags in reduce.
This was a source of slowdown observed in bedrock2.
Diffstat (limited to 'tactics/redexpr.ml')
0 files changed, 0 insertions, 0 deletions