diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean index a5eb30c4f0..c57b7a72f5 100644 --- a/src/Lean/Compiler/LCNF/Passes.lean +++ b/src/Lean/Compiler/LCNF/Passes.lean @@ -42,10 +42,10 @@ def saveMono : Pass := def builtinPassManager : PassManager := { passes := #[ - init -/- + init, pullInstances, - cse, + cse +/- simp, floatLetIn, findJoinPoints, diff --git a/src/Lean/Compiler/LCNF/PullLetDecls.lean b/src/Lean/Compiler/LCNF/PullLetDecls.lean index 47ff2eb4d2..b80174336c 100644 --- a/src/Lean/Compiler/LCNF/PullLetDecls.lean +++ b/src/Lean/Compiler/LCNF/PullLetDecls.lean @@ -8,10 +8,6 @@ import Lean.Compiler.LCNF.DependsOn import Lean.Compiler.LCNF.Types import Lean.Compiler.LCNF.PassManager - -set_option warningAsError false -#exit - namespace Lean.Compiler.LCNF namespace PullLetDecls @@ -107,7 +103,7 @@ def Decl.pullInstances (decl : Decl) : CompilerM Decl := decl.pullLetDecls fun letDecl candidates => do if (← isClass? letDecl.type).isSome then return true - else if let .proj _ _ (.fvar fvarId) := letDecl.value then + else if let .proj _ _ fvarId := letDecl.value then return candidates.contains fvarId else return false