From 7c5d91ebc3b82c6f73ca144960b31b3d47dd3765 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 30 Nov 2022 06:31:03 -0800 Subject: [PATCH] fix: avoid `hygienic ++ hygienic` at `Specialize.lean` --- src/Lean/Compiler/LCNF/Specialize.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/Specialize.lean b/src/Lean/Compiler/LCNF/Specialize.lean index 5145651fb36..1149e1ddea7 100644 --- a/src/Lean/Compiler/LCNF/Specialize.lean +++ b/src/Lean/Compiler/LCNF/Specialize.lean @@ -207,7 +207,7 @@ Specialize `decl` using - `levelParamsNew`: the universe level parameters for the new declaration. -/ def mkSpecDecl (decl : Decl) (us : List Level) (argMask : Array (Option Arg)) (params : Array Param) (decls : Array CodeDecl) (levelParamsNew : List Name) : SpecializeM Decl := do - let nameNew := decl.name ++ `_at_ ++ (← read).declName ++ (`spec).appendIndexAfter (← get).decls.size + let nameNew := decl.name ++ `_at_ ++ (← read).declName.eraseMacroScopes ++ (`spec).appendIndexAfter (← get).decls.size /- Recall that we have just retrieved `decl` using `getDecl?`, and it may have free variable identifiers that overlap with the free-variables in `params` and `decls` (i.e., the "closure").