diff --git a/src/Lean/Meta/Tactic/Cbv/Main.lean b/src/Lean/Meta/Tactic/Cbv/Main.lean index f1f43bdb91..f12ce75019 100644 --- a/src/Lean/Meta/Tactic/Cbv/Main.lean +++ b/src/Lean/Meta/Tactic/Cbv/Main.lean @@ -145,7 +145,7 @@ def cbvPre : Simproc := isBuiltinValue <|> isProofTerm <|> skipBinders >> isOpaqueApp >> simpControlCbv - <|> ((isOpaqueConst >> handleConst) <|> simplifyAppFn <|> handleProj) + <|> ((isOpaqueConst >> handleConst) <|> simplifyAppFn <|> handleProj) <|> zetaReduce def cbvPost : Simproc := evalGround