max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add profileitM for simp

Browse source
This commit is contained in:
Leonardo de Moura 2021-03-04 17:27:01 -08:00
parent a81c628a12
commit db499a646f
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/Tactic/Simp/Main.lean
View file

@ -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