From 6703af1ea02c07167cc7e97ff4e997710f8c0a45 Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Fri, 23 May 2025 21:07:19 -0700 Subject: [PATCH] chore: rename closed term suffix from _closedTerm to _closed The longer name was chosen to avoid clashes with the old compiler. --- src/Lean/Compiler/LCNF/ExtractClosed.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/ExtractClosed.lean b/src/Lean/Compiler/LCNF/ExtractClosed.lean index 80b766cef1..1ef4044c95 100644 --- a/src/Lean/Compiler/LCNF/ExtractClosed.lean +++ b/src/Lean/Compiler/LCNF/ExtractClosed.lean @@ -111,7 +111,7 @@ partial def visitCode (code : Code) : M Code := do eraseCode closedCode pure closedTermName else - let name := (← read).baseName ++ (`_closedTerm).appendIndexAfter (← get).decls.size + let name := (← read).baseName ++ (`_closed).appendIndexAfter (← get).decls.size cacheClosedTermName env closedExpr name |> setEnv let decl := { name, levelParams := [], type := decl.type, params := #[], value := .code closedCode, inlineAttr? := some .noinline }