diff options
Diffstat (limited to 'theories/Init/Tactics.v')
| -rw-r--r-- | theories/Init/Tactics.v | 7 |
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. |