diff --git a/src/Lean/PrettyPrinter/Delaborator/Options.lean b/src/Lean/PrettyPrinter/Delaborator/Options.lean
index 1668c09883a7..54bd2f7ee31e 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Options.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Options.lean
@@ -39,11 +39,11 @@ register_builtin_option pp.unicode.fun : Bool := {
 }
 register_builtin_option pp.match : Bool := {
   defValue := true
-  descr    := "(pretty printer) disable/enable 'match' notation"
+  descr    := "(pretty printer) disable/enable `match` notation"
 }
 register_builtin_option pp.sorrySource : Bool := {
   defValue := false
-  descr    := "(pretty printer) if true, pretty print 'sorry' with its originating source position, if available"
+  descr    := "(pretty printer) if true, pretty print `sorry` with its originating source position, if available"
 }
 register_builtin_option pp.coercions : Bool := {
   defValue := true
diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index 790ceaaf34c0..a73d0af094c4 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -50,17 +50,17 @@ register_builtin_option pp.analyze.typeAscriptions : Bool := {
 
 register_builtin_option pp.analyze.trustSubst : Bool := {
   defValue := false
-  descr    := "(pretty printer analyzer) always 'pretend' applications that can delab to ▸ are 'regular'"
+  descr    := "(pretty printer analyzer) always \"pretend\" applications that can delab to ▸ are \"regular\""
 }
 
 register_builtin_option pp.analyze.trustOfNat : Bool := {
   defValue := true
-  descr    := "(pretty printer analyzer) always 'pretend' `OfNat.ofNat` applications can elab bottom-up"
+  descr    := "(pretty printer analyzer) always \"pretend\" `OfNat.ofNat` applications can elab bottom-up"
 }
 
 register_builtin_option pp.analyze.trustOfScientific : Bool := {
   defValue := true
-  descr    := "(pretty printer analyzer) always 'pretend' `OfScientific.ofScientific` applications can elab bottom-up"
+  descr    := "(pretty printer analyzer) always \"pretend\" `OfScientific.ofScientific` applications can elab bottom-up"
 }
 
 -- TODO: this is an arbitrary special case of a more general principle.