From e56bf66d8da1b328177a907ddf57277c4b4efc9d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 10 Apr 2021 16:09:04 -0700
Subject: [PATCH] chore: rename option `hygienicIntro` ==> `tactic.hygienic`

It is easier to find.
---
 src/Lean/Meta/Tactic/Intro.lean | 6 +++---
 tests/lean/hygienicIntro.lean   | 4 ++--
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Intro.lean b/src/Lean/Meta/Tactic/Intro.lean
index 51be4d32e1..c3c1796bbd 100644
--- a/src/Lean/Meta/Tactic/Intro.lean
+++ b/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)
diff --git a/tests/lean/hygienicIntro.lean b/tests/lean/hygienicIntro.lean
index 90eade0cd7..d8c808d97c 100644
--- a/tests/lean/hygienicIntro.lean
+++ b/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