diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean index 795eede4eb..95b167d52f 100644 --- a/src/Lean/Compiler/LCNF/Passes.lean +++ b/src/Lean/Compiler/LCNF/Passes.lean @@ -17,9 +17,16 @@ namespace Lean.Compiler.LCNF open PassInstaller +def init : Pass where + name := `init + run := fun decls => do + decls.forM (ยท.saveBase) + return decls + phase := .base + def builtinPassManager : PassManager := { passes := #[ - { name := `init, run := pure, phase := .base }, + init, pullInstances, cse, simp,