diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 52df5bec85..3c00e05c5f 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -196,6 +196,9 @@ do fmt ← pp a,
 meta def trace_call_stack : tactic unit :=
 take state, _root_.trace_call_stack (success () state)
 
+meta def timetac {α : Type u} (desc : string) (t : tactic α) : tactic α :=
+λ s, timeit desc (t s)
+
 meta def trace_state : tactic unit :=
 do s ← read,
    trace $ to_fmt s