diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp
index c355206f2..5a6299cb0 100644
--- a/src/frontends/lean/info_manager.cpp
+++ b/src/frontends/lean/info_manager.cpp
@@ -187,7 +187,7 @@ public:
     virtual void display(io_state_stream const & ios, unsigned line) const {
         ios << "-- COERCION|" << line << "|" << get_column() << "\n";
         options os = ios.get_options();
-        os = os.update(get_pp_coercion_option_name(), true);
+        os = os.update(get_pp_coercions_option_name(), true);
         ios.update_options(os) << m_expr << endl << "--" << endl << m_type << endl;
         ios << "-- ACK" << endl;
     }
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 006c8af39..aa669cee4 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -114,7 +114,7 @@ void pretty_fn::set_options_core(options const & o) {
     m_max_steps     = get_pp_max_steps(o);
     m_implict       = get_pp_implicit(o);
     m_unicode       = get_pp_unicode(o);
-    m_coercion      = get_pp_coercion(o);
+    m_coercion      = get_pp_coercions(o);
     m_notation      = get_pp_notation(o);
     m_universes     = get_pp_universes(o);
     m_full_names    = get_pp_full_names(o);
diff --git a/src/frontends/lean/pp_options.cpp b/src/frontends/lean/pp_options.cpp
index 85d8a23d2..42526552b 100644
--- a/src/frontends/lean/pp_options.cpp
+++ b/src/frontends/lean/pp_options.cpp
@@ -22,8 +22,8 @@ Author: Leonardo de Moura
 #define LEAN_DEFAULT_PP_IMPLICIT false
 #endif
 
-#ifndef LEAN_DEFAULT_PP_COERCION
-#define LEAN_DEFAULT_PP_COERCION false
+#ifndef LEAN_DEFAULT_PP_COERCIONS
+#define LEAN_DEFAULT_PP_COERCIONS false
 #endif
 
 #ifndef LEAN_DEFAULT_PP_UNIVERSES
@@ -47,24 +47,24 @@ static name g_pp_max_depth        {"pp", "max_depth"};
 static name g_pp_max_steps        {"pp", "max_steps"};
 static name g_pp_notation         {"pp", "notation"};
 static name g_pp_implicit         {"pp", "implicit"};
-static name g_pp_coercion         {"pp", "coercion"};
+static name g_pp_coercions        {"pp", "coercions"};
 static name g_pp_universes        {"pp", "universes"};
 static name g_pp_full_names       {"pp", "full_names"};
 static name g_pp_private_names    {"pp", "private_names"};
 static name g_pp_metavar_args     {"pp", "metavar_args"};
 
-name const & get_pp_coercion_option_name() { return g_pp_coercion; }
+name const & get_pp_coercions_option_name() { return g_pp_coercions; }
 name const & get_pp_full_names_option_name() { return g_pp_full_names; }
 
 list<options> const & get_distinguishing_pp_options() {
     static options g_universes_true(g_pp_universes, true);
     static options g_implicit_true(g_pp_implicit, true);
-    static options g_coercion_true(g_pp_coercion, true);
+    static options g_coercions_true(g_pp_coercions, true);
     static options g_notation_false(g_pp_notation, false);
-    static options g_implicit_coercion = join(g_coercion_true, g_implicit_true);
+    static options g_implicit_coercions = join(g_coercions_true, g_implicit_true);
     static options g_implicit_notation = join(g_notation_false, g_implicit_true);
-    static options g_all = join(join(g_universes_true, g_implicit_true), join(g_coercion_true, g_notation_false));
-    static list<options> g_distinguishing_pp_options({g_implicit_true, g_coercion_true, g_implicit_coercion, g_implicit_notation, g_universes_true, g_all});
+    static options g_all = join(join(g_universes_true, g_implicit_true), join(g_coercions_true, g_notation_false));
+    static list<options> g_distinguishing_pp_options({g_implicit_true, g_coercions_true, g_implicit_coercions, g_implicit_notation, g_universes_true, g_all});
     return g_distinguishing_pp_options;
 }
 
@@ -76,8 +76,8 @@ RegisterBoolOption(g_pp_notation,  LEAN_DEFAULT_PP_NOTATION,
                    "(pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)");
 RegisterBoolOption(g_pp_implicit,  LEAN_DEFAULT_PP_IMPLICIT,
                    "(pretty printer) display implicit parameters");
-RegisterBoolOption(g_pp_coercion,  LEAN_DEFAULT_PP_COERCION,
-                   "(pretty printer) display coercions");
+RegisterBoolOption(g_pp_coercions,  LEAN_DEFAULT_PP_COERCIONS,
+                   "(pretty printer) display coercionss");
 RegisterBoolOption(g_pp_universes,  LEAN_DEFAULT_PP_UNIVERSES,
                    "(pretty printer) display universes");
 RegisterBoolOption(g_pp_full_names,  LEAN_DEFAULT_PP_FULL_NAMES,
@@ -91,7 +91,7 @@ unsigned get_pp_max_depth(options const & opts)     { return opts.get_unsigned(g
 unsigned get_pp_max_steps(options const & opts)     { return opts.get_unsigned(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); }
 bool     get_pp_notation(options const & opts)      { return opts.get_bool(g_pp_notation, LEAN_DEFAULT_PP_NOTATION); }
 bool     get_pp_implicit(options const & opts)      { return opts.get_bool(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT); }
-bool     get_pp_coercion(options const & opts)      { return opts.get_bool(g_pp_coercion, LEAN_DEFAULT_PP_COERCION); }
+bool     get_pp_coercions(options const & opts)     { return opts.get_bool(g_pp_coercions, LEAN_DEFAULT_PP_COERCIONS); }
 bool     get_pp_universes(options const & opts)     { return opts.get_bool(g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES); }
 bool     get_pp_full_names(options const & opts)    { return opts.get_bool(g_pp_full_names, LEAN_DEFAULT_PP_FULL_NAMES); }
 bool     get_pp_private_names(options const & opts) { return opts.get_bool(g_pp_private_names, LEAN_DEFAULT_PP_PRIVATE_NAMES); }
diff --git a/src/frontends/lean/pp_options.h b/src/frontends/lean/pp_options.h
index 0031898da..6aa2c1022 100644
--- a/src/frontends/lean/pp_options.h
+++ b/src/frontends/lean/pp_options.h
@@ -7,14 +7,14 @@ Author: Leonardo de Moura
 #pragma once
 #include "util/sexpr/options.h"
 namespace lean {
-name const & get_pp_coercion_option_name();
+name const & get_pp_coercions_option_name();
 name const & get_pp_full_names_option_name();
 
 unsigned get_pp_max_depth(options const & opts);
 unsigned get_pp_max_steps(options const & opts);
 bool     get_pp_notation(options const & opts);
 bool     get_pp_implicit(options const & opts);
-bool     get_pp_coercion(options const & opts);
+bool     get_pp_coercions(options const & opts);
 bool     get_pp_universes(options const & opts);
 bool     get_pp_full_names(options const & opts);
 bool     get_pp_private_names(options const & opts);
diff --git a/tests/lean/run/choice_ctx.lean b/tests/lean/run/choice_ctx.lean
index e3f524294..b977c7f18 100644
--- a/tests/lean/run/choice_ctx.lean
+++ b/tests/lean/run/choice_ctx.lean
@@ -1,7 +1,7 @@
 import data.nat.basic
 open nat
 open eq
-set_option pp.coercion true
+set_option pp.coercions true
 
 namespace foo
 theorem trans {a b c : nat} (H1 : a = b) (H2 : b = c) : a = c :=
diff --git a/tests/lean/run/class_coe.lean b/tests/lean/run/class_coe.lean
index 32e4cedc7..ac3b5633c 100644
--- a/tests/lean/run/class_coe.lean
+++ b/tests/lean/run/class_coe.lean
@@ -29,7 +29,7 @@ coercion nat_to_int
 coercion int_to_real
 
 set_option pp.implicit true
-set_option pp.coercion true
+set_option pp.coercions true
 check n + m
 check i + j
 check x + y
diff --git a/tests/lean/run/coe1.lean b/tests/lean/run/coe1.lean
index a2abf1369..3b42849ce 100644
--- a/tests/lean/run/coe1.lean
+++ b/tests/lean/run/coe1.lean
@@ -6,7 +6,7 @@ variable g : B → B → B
 variables a1 a2 a3 : A
 variables b1 b2 b3 : B
 check g a1 b1
-set_option pp.coercion true
+set_option pp.coercions true
 check g a1 b1
 
 variable eq {A : Type} : A → A → Type.{0}
diff --git a/tests/lean/run/coe6.lean b/tests/lean/run/coe6.lean
index b97f520a7..2c3af9f22 100644
--- a/tests/lean/run/coe6.lean
+++ b/tests/lean/run/coe6.lean
@@ -10,6 +10,6 @@ variable nsucc : nat → nat
 definition f [coercion] (a : unit) : int := izero
 definition g [coercion] (a : unit) : nat := nzero
 
-set_option pp.coercion true
+set_option pp.coercions true
 check isucc star
 check nsucc star