From db499a646f5fbfbc2788c426cf4106d61101f193 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Mar 2021 17:27:01 -0800 Subject: [PATCH] chore: add `profileitM` for `simp` --- src/Lean/Meta/Tactic/Simp/Main.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index 423bc51010..629c94861f 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -350,7 +350,7 @@ end DefaultMethods end Simp -def simp (e : Expr) (ctx : Simp.Context) : MetaM Simp.Result := do +def simp (e : Expr) (ctx : Simp.Context) : MetaM Simp.Result := do profileitM Exception "simp" (← getOptions) do Simp.main e ctx (methods := Simp.DefaultMethods.methods) end Lean.Meta