diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 94f111fd9c..5e929cf00f 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -72,6 +72,7 @@ struct structure_cmd_fn {
     buffer<expr>               m_params;
     expr                       m_type;
     buffer<expr>               m_parents;
+    buffer<bool>               m_private_parents;
     name                       m_mk;
     pos_info                   m_mk_pos;
     implicit_infer_kind        m_mk_infer;
@@ -153,8 +154,14 @@ struct structure_cmd_fn {
             m_p.next();
             while (true) {
                 auto pos = m_p.pos();
+                bool is_private_parent = false;
+                if (m_p.curr_is_token(get_private_tk())) {
+                    m_p.next();
+                    is_private_parent  = true;
+                }
                 expr parent = m_p.parse_expr();
                 m_parents.push_back(parent);
+                m_private_parents.push_back(is_private_parent);
                 check_parent(parent, pos);
                 name const & parent_name = const_name(get_app_fn(parent));
                 auto parent_info         = get_parent_info(parent_name);
@@ -656,10 +663,12 @@ struct structure_cmd_fn {
             m_env = set_reducible(m_env, coercion_name, reducible_status::On);
             save_def_info(coercion_name);
             add_alias(coercion_name);
-            m_env = add_coercion(m_env, coercion_name, m_p.ios());
-            if (m_modifiers.is_class() && is_class(m_env, parent_name)) {
-                // if both are classes, then we also mark coercion_name as an instance
-                m_env = add_instance(m_env, coercion_name);
+            if (!m_private_parents[i]) {
+                m_env = add_coercion(m_env, coercion_name, m_p.ios());
+                if (m_modifiers.is_class() && is_class(m_env, parent_name)) {
+                    // if both are classes, then we also mark coercion_name as an instance
+                    m_env = add_instance(m_env, coercion_name);
+                }
             }
         }
     }
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index 4e191063e8..93e6b50637 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -62,6 +62,7 @@ static name * g_proof        = nullptr;
 static name * g_qed          = nullptr;
 static name * g_begin        = nullptr;
 static name * g_end          = nullptr;
+static name * g_private      = nullptr;
 static name * g_definition   = nullptr;
 static name * g_theorem      = nullptr;
 static name * g_axiom        = nullptr;
@@ -147,6 +148,7 @@ void initialize_tokens() {
     g_qed          = new name("qed");
     g_begin        = new name("begin");
     g_end          = new name("end");
+    g_private      = new name("private");
     g_definition   = new name("definition");
     g_theorem      = new name("theorem");
     g_opaque       = new name("opaque");
@@ -195,6 +197,7 @@ void finalize_tokens() {
     delete g_call;
     delete g_with;
     delete g_class;
+    delete g_private;
     delete g_definition;
     delete g_theorem;
     delete g_opaque;
@@ -318,6 +321,7 @@ name const & get_proof_tk() { return *g_proof; }
 name const & get_qed_tk() { return *g_qed; }
 name const & get_begin_tk() { return *g_begin; }
 name const & get_end_tk() { return *g_end; }
+name const & get_private_tk() { return *g_private; }
 name const & get_definition_tk() { return *g_definition; }
 name const & get_theorem_tk() { return *g_theorem; }
 name const & get_axiom_tk() { return *g_axiom; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index 13ee6a8433..ae81896935 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -64,6 +64,7 @@ name const & get_proof_tk();
 name const & get_begin_tk();
 name const & get_qed_tk();
 name const & get_end_tk();
+name const & get_private_tk();
 name const & get_definition_tk();
 name const & get_theorem_tk();
 name const & get_axiom_tk();
diff --git a/tests/lean/run/record6.lean b/tests/lean/run/record6.lean
new file mode 100644
index 0000000000..902cbab985
--- /dev/null
+++ b/tests/lean/run/record6.lean
@@ -0,0 +1,14 @@
+import logic data.unit
+
+structure point (A : Type) (B : Type) :=
+mk :: (x : A) (y : B)
+
+structure point2 (A : Type) (B : Type) extends point A B :=
+make
+
+structure point3 extends point num num, private point2 num num renaming x→y y→z
+
+check point3.mk
+
+theorem tst : point3.mk 1 2 3 = point.mk 1 2 :=
+rfl