diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean index 0a2aed6e1a..5a1b7cb3c6 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -31,7 +31,7 @@ open Meta SubExpr register_builtin_option pp.analyze : Bool := { defValue := false group := "pp.analyze" - descr := "(pretty printer analyzer) determine annotations sufficient to ensure round-tripping" + descr := "(pretty printer analyzer) try to determine annotations sufficient to ensure round-tripping" } register_builtin_option pp.analyze.checkInstances : Bool := {