diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 3943c5dfae..bb1d011680 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -667,9 +667,9 @@ private def checkUnsupported [Monad m] [MonadEnv m] [MonadError m] (decl : Decla | _ => pure () register_builtin_option compiler.enableNew : Bool := { - defValue := false + defValue := true group := "compiler" - descr := "(compiler) enable the new code generator, this should have no significant effect on your code but it does help to test the new code generator; unset to only use the old code generator instead" + descr := "(compiler) enable the new code generator, unset to use the old code generator instead" } /--