feat: option for disabling hygiene

/cc @leodemoura

src/Lean/Elab/Quotation.lean

@@ -17,6 +17,11 @@ open Lean.Parser.Term
 open Lean.Syntax
 open Meta
 
+register_builtin_option hygiene : Bool := {
+  defValue := true
+  descr    := "Annotate identifiers in quotations such that they are resolved relative to the scope at their declaration, not that at their eventual use/expansion, to avoid accidental capturing. Note that quotations/notations already defined are unaffected."
+}
+
 /-- `C[$(e)]` ~> `let a := e; C[$a]`. Used in the implementation of antiquot splices. -/
 private partial def floatOutAntiquotTerms : Syntax → StateT (Syntax → TermElabM Syntax) TermElabM Syntax
   | stx@(Syntax.node k args) => do
@@ -57,6 +62,8 @@ def resolveSectionVariable (sectionVars : NameMap Name) (id : Name) : List (Name
 -- Elaborate the content of a syntax quotation term
 private partial def quoteSyntax : Syntax → TermElabM Syntax
   | Syntax.ident info rawVal val preresolved => do
+    if !hygiene.get (← getOptions) then
+      return ← `(Syntax.ident info $(quote rawVal) $(quote val) $(quote preresolved))
     -- Add global scopes at compilation time (now), add macro scope at runtime (in the quotation).
     -- See the paper for details.
     let r ← resolveGlobalName val

tests/lean/unhygienic.lean

@@ -0,0 +1,19 @@
+set_option hygiene false in
+notation "X" => x
+
+def x : Bool := true
+#check X
+#check fun (x : Nat) => X
+
+notation "Y" => fun (x : Nat) => X
+#check fun (x : Int) => Y
+
+
+variable (Com State : Type)
+variable (skip : Com)
+
+set_option hygiene false in
+notation:60 cs " ⇓ " σ' " : " steps:60 => Bigstep cs σ' steps
+
+inductive Bigstep : Com × State → State → Nat → Prop where
+  | skip {σ} : ⟨skip, σ⟩ ⇓ σ : 1

tests/lean/unhygienic.lean.expected.out

@@ -0,0 +1,3 @@
+x : Bool
+fun (x : Nat) => x : Nat → Nat
+fun (x : Int) (x_1 : Nat) => x : Int → Nat → Int