aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-12-11 05:21:05 -0500
committerGravatar Jason Gross <jgross@mit.edu>2017-12-14 12:19:02 -0500
commit90d79c5656c394909ffc9343b903dd1231abd7a4 (patch)
tree0aec14a5e6547173a47482a3e4d10780828a905d /theories/Init
parent6734614d8ace6860e3deb1861611ba4b012cfae1 (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 'theories/Init')
-rw-r--r--theories/Init/Tactics.v7
1 files changed, 7 insertions, 0 deletions
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 5d0e7602a..47a971ef0 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -306,3 +306,10 @@ Ltac inversion_sigma_step :=
=> induction_sigma_in_using H @eq_sigT2_rect
end.
Ltac inversion_sigma := repeat inversion_sigma_step.
+
+(** A version of [time] that works for constrs *)
+Ltac time_constr tac :=
+ let eval_early := match goal with _ => restart_timer end in
+ let ret := tac () in
+ let eval_early := match goal with _ => finish_timing ( "Tactic evaluation" ) end in
+ ret.