diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-12-11 05:21:05 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-12-14 12:19:02 -0500 |
| commit | 90d79c5656c394909ffc9343b903dd1231abd7a4 (patch) | |
| tree | 0aec14a5e6547173a47482a3e4d10780828a905d /CHANGES | |
| parent | 6734614d8ace6860e3deb1861611ba4b012cfae1 (diff) | |
Add named timers to LtacProf
I'm not sure if they belong in profile_ltac, or in extratactics, or,
perhaps, in a separate plugin. But I'd find it very useful to have a
version of `time` that works on constr evaluation, which is what this
commit provides.
I'm not sure that I've picked good naming conventions for the tactics,
either.
Diffstat (limited to 'CHANGES')
0 files changed, 0 insertions, 0 deletions