From a0bb5f4961b9b5326ac21d6f4cd8a8a88cf1024f Mon Sep 17 00:00:00 2001
From: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Date: Wed, 2 Jul 2025 20:46:21 +0200
Subject: [PATCH] chore: fixes for #9158 after stage0 update (#9161)

---
 src/Lean/Elab/Tactic/Grind.lean      | 2 --
 src/Lean/Meta/Tactic/Grind/Attr.lean | 2 --
 2 files changed, 4 deletions(-)

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