diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index d3e626190..e320abc9b 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -167,7 +167,7 @@ bool is_alias_decl(object const & obj) {
 }
 
 bool supported_by_pp(object const & obj) {
-    return obj.kind() != object_kind::Neutral || is_notation_decl(obj) || is_coercion_decl(obj) || is_alias_decl(obj);
+    return obj.kind() != object_kind::Neutral || is_notation_decl(obj) || is_coercion_decl(obj) || is_alias_decl(obj) || is_set_opaque(obj);
 }
 
 /** \brief Functional object for pretty printing expressions */
@@ -1374,6 +1374,11 @@ class pp_formatter_cell : public formatter_cell {
         format d_fmt   = is_constant(d) ? format(const_name(d)) : pp(d, opts);
         return format{highlight_command(format(alias_decl.keyword())), space(), ::lean::pp(n), space(), colon(), space(), d_fmt};
     }
+
+    format pp_set_opaque(object const & obj) {
+        return format{highlight_command(format(obj.keyword())), space(), format(get_set_opaque_id(obj)), space(),
+                format(get_set_opaque_flag(obj) ? "true" : "false")};
+    }
 public:
     pp_formatter_cell(ro_environment const & env):
         m_env(env) {
@@ -1418,6 +1423,8 @@ public:
                 return pp_coercion_decl(obj, opts);
             } else if (is_alias_decl(obj)) {
                 return pp_alias_decl(obj, opts);
+            } else if (is_set_opaque(obj)) {
+                return pp_set_opaque(obj);
             } else {
                 // If the object is not notation or coercion
                 // declaration, then the object was created in
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index c4f0f7791..e96e3e21d 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -35,6 +35,8 @@ public:
     virtual ~set_opaque_command() {}
     virtual char const * keyword() const { return "SetOpaque"; }
     virtual void write(serializer & s) const { s << "Opa" << m_obj_name << m_opaque; }
+    name const & get_obj_name() const { return m_obj_name; }
+    bool get_flag() const { return m_opaque; }
 };
 static void read_set_opaque(environment const & env, io_state const &, deserializer & d) {
     name n = read_name(d);
@@ -43,6 +45,20 @@ static void read_set_opaque(environment const & env, io_state const &, deseriali
 }
 static object_cell::register_deserializer_fn set_opaque_ds("Opa", read_set_opaque);
 
+bool is_set_opaque(object const & obj) {
+    return dynamic_cast<set_opaque_command const *>(obj.cell());
+}
+
+name const & get_set_opaque_id(object const & obj) {
+    lean_assert(is_set_opaque(obj));
+    return static_cast<set_opaque_command const *>(obj.cell())->get_obj_name();
+}
+
+bool get_set_opaque_flag(object const & obj) {
+    lean_assert(is_set_opaque(obj));
+    return static_cast<set_opaque_command const *>(obj.cell())->get_flag();
+}
+
 class import_command : public neutral_object_cell {
     std::string m_mod_name;
 public:
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index d5459a713..c0fd83817 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -429,4 +429,19 @@ struct register_builtin_fn {
    Return none if there is no builtin associated the given name.
 */
 optional<std::pair<expr, bool>> get_builtin(name const & n);
+
+/**
+   \brief Return true iff \c obj is a SetOpaque command mark.
+*/
+bool is_set_opaque(object const & obj);
+/**
+   \brief Return the identifier of a SetOpaque command.
+   \pre is_set_opaque(obj)
+*/
+name const & get_set_opaque_id(object const & obj);
+/**
+   \brief Return the flag of a SetOpaque command.
+   \pre is_set_opaque(obj)
+*/
+bool get_set_opaque_flag(object const & obj);
 }