chore: make auto param decls of private decls private

Author: Kha

src/Lean/Elab/Binders.lean

@@ -92,7 +92,7 @@ Returns the declaration name.
 -/
 def declareTacticSyntax (tactic : Syntax) (name? : Option Name := none) : TermElabM Name :=
   withFreshMacroScope do
-    let name ← name?.getDM do MonadQuotation.addMacroScope ((← getEnv).asyncPrefix?.getD .anonymous ++ `_auto)
+    let name ← name?.getDM (mkAuxDeclName `_auto)
     let type := Lean.mkConst `Lean.Syntax
     let value ← quoteAutoTactic tactic
     trace[Elab.autoParam] value

tests/lean/run/3257.lean

@@ -15,7 +15,7 @@ example : U := by
 
 /--
 trace: [Meta.Tactic.simp.discharge] bar discharge ✅️
-      autoParam T _auto✝
+      autoParam T bar._auto_1
   [Meta.Tactic.simp.rewrite] T.mk:1000:
         T
       ==>

tests/lean/run/cleanup_forallTelescope.lean

@@ -29,7 +29,7 @@ def f (x := 0) (_ : x = x := by rfl) : Nat := x+1
 
 
 /--
-info: (x : optParam Nat 0) → autoParam (x = x) _auto✝ → Nat
+info: (x : optParam Nat 0) → autoParam (x = x) f._auto_1 → Nat
 ---
 (x : Nat) → x = x → Nat
 -/