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.

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.