diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean index 5ff735e9da17..82a447c0d393 100644 --- a/src/Lean/Meta/InferType.lean +++ b/src/Lean/Meta/InferType.lean @@ -187,7 +187,7 @@ because it overrides unrelated configurations. @[inline] def withInferTypeConfig (x : MetaM α) : MetaM α := withAtLeastTransparency .default do let cfg ← getConfig - if cfg.beta && cfg.iota && cfg.zeta && cfg.zetaDelta && cfg.proj != .no then + if cfg.beta && cfg.iota && cfg.zeta && cfg.zetaDelta && cfg.proj == .yesWithDelta then x else withConfig (fun cfg => { cfg with beta := true, iota := true, zeta := true, zetaDelta := true, proj := .yesWithDelta }) x