diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean index 33aefdc4b8..3bfee21ea7 100644 --- a/src/Lean/Compiler/LCNF/Passes.lean +++ b/src/Lean/Compiler/LCNF/Passes.lean @@ -45,6 +45,7 @@ def builtinPassManager : PassManager := { init, pullInstances, cse, +/- simp, floatLetIn, findJoinPoints, @@ -55,7 +56,9 @@ def builtinPassManager : PassManager := { specialize, simp (occurrence := 2), cse (occurrence := 1), +-/ saveBase, -- End of base phase +/- toMono, simp (occurrence := 3) (phase := .mono), reduceJpArity (phase := .mono), @@ -69,6 +72,7 @@ def builtinPassManager : PassManager := { extendJoinPointContext (phase := .mono) (occurrence := 1), simp (occurrence := 5) (phase := .mono), cse (occurrence := 2) (phase := .mono), +-/ saveMono -- End of mono phase ] }