Double-quoted names are not hygienic #586
Description
open Nat in
macro "foo" : command => `(
#check zero
#check ``succ)
foo
-- Nat.zero : Nat
-- unknown constant 'succ'
macro "bar" : command => `(
#check zero
#check ``succ)
open Nat in
bar
-- unknown identifier 'zero'
-- `Nat.succ : Lean.NameThis is because they are not made of Syntax.idents, so our hygiene algorithm cannot store the extra-macro context in preresolved