diff --git a/src/Lean/Elab/Tactic/Grind.lean b/src/Lean/Elab/Tactic/Grind.lean index d6054884ce..1d8a8ba502 100644 --- a/src/Lean/Elab/Tactic/Grind.lean +++ b/src/Lean/Elab/Tactic/Grind.lean @@ -12,8 +12,6 @@ import Lean.Elab.MutualDef import Lean.Elab.Tactic.Basic import Lean.Elab.Tactic.Config -set_option interpreter.prefer_native false -- TODO: remove - namespace Lean.Elab.Tactic open Meta diff --git a/src/Lean/Meta/Tactic/Grind/Attr.lean b/src/Lean/Meta/Tactic/Grind/Attr.lean index 5a6d85055f..e71920c46e 100644 --- a/src/Lean/Meta/Tactic/Grind/Attr.lean +++ b/src/Lean/Meta/Tactic/Grind/Attr.lean @@ -17,8 +17,6 @@ inductive AttrKind where | infer | ext -set_option interpreter.prefer_native false -- TODO: remove - /-- Return theorem kind for `stx` of the form `Attr.grindThmMod` -/ def getAttrKindCore (stx : Syntax) : CoreM AttrKind := do match stx with