From 90d79c5656c394909ffc9343b903dd1231abd7a4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 11 Dec 2017 05:21:05 -0500 Subject: 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. --- theories/Init/Tactics.v | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'theories') 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. -- cgit v1.2.3