chore: rename option hygienicIntro ==> tactic.hygienic

It is easier to find.

src/Lean/Meta/Tactic/Intro.lean

@@ -55,14 +55,14 @@ namespace Lean.Meta
   let (fvars, mvarId) ← loop n lctx #[] 0 s mvarType
   pure (fvars.map Expr.fvarId!, mvarId)
 
-register_builtin_option hygienicIntro : Bool := {
+register_builtin_option tactic.hygienic : Bool := {
   defValue := true
   group    := "tactic"
-  descr    := "make sure 'intro'-like tactics are hygienic"
+  descr    := "make sure tactics are hygienic"
 }
 
 def getHygienicIntro : MetaM Bool := do
-  return hygienicIntro.get (← getOptions)
+  return tactic.hygienic.get (← getOptions)
 
 private def mkAuxNameImp (preserveBinderNames : Bool) (hygienic : Bool) (useNamesForExplicitOnly : Bool)
     (lctx : LocalContext) (binderName : Name) (isExplicit : Bool) : List Name → MetaM (Name × List Name)

tests/lean/hygienicIntro.lean

@@ -1,6 +1,6 @@
 --
 
-set_option hygienicIntro false in
+set_option tactic.hygienic false in
 theorem ex1 {a p q r : Prop} : p → (p → q) → (q → r) → r := by
 intro _ h1 h2;
 apply h2;
@@ -24,7 +24,7 @@ example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by
   { apply h₁; exact h }; -- error "unknown identifier"
   exact h
 
-set_option hygienicIntro false in
+set_option tactic.hygienic false in
 example {p q : Prop} (h₁ : p → q) (h₂ : p ∨ q) : q := by
 cases h₂;
 { apply h₁; exact h }; -- hygiene is disabled