test: add test for local macro in auto tactic

tests/pkg/misc/Misc.lean

@@ -10,3 +10,6 @@ open Lean Meta
   IO.println <| (← getEnv).getModuleIdxFor? ``foo
   IO.println <| (← getEnv).getModuleIdxFor? `auxDecl1
   IO.println "worked"
+
+set_option pp.all true
+#check f 10 10

tests/pkg/misc/Misc/Foo.lean

@@ -11,3 +11,8 @@ def foo := 42
 local infix:50 " ≺ " => LE.le
 
 #check 1 ≺ 2
+
+local macro "my_refl" : tactic =>
+  `(tactic| rfl)
+
+def f (x y : Nat) (_h : x = y := by my_refl) := x