From 186d910d0b1e64436ed8a228bfd8d911a044211b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 3 Nov 2014 17:55:59 -0800
Subject: [PATCH] feat(frontends/lean/structure_cmd): mark coercion to parents
 as coercions and instances (when both structures as classes)

---
 src/frontends/lean/structure_cmd.cpp |  6 ++++++
 tests/lean/run/record3.lean          | 17 +++++++++++++++++
 2 files changed, 23 insertions(+)
 create mode 100644 tests/lean/run/record3.lean

diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index c40e52767..7c5a34fab 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -22,6 +22,7 @@ Author: Leonardo de Moura
 #include "library/unifier.h"
 #include "library/module.h"
 #include "library/aliases.h"
+#include "library/coercion.h"
 #include "library/explicit.h"
 #include "library/protected.h"
 #include "library/definitional/rec_on.h"
@@ -641,6 +642,11 @@ 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);
+            }
         }
     }
 
diff --git a/tests/lean/run/record3.lean b/tests/lean/run/record3.lean
new file mode 100644
index 000000000..a413feadf
--- /dev/null
+++ b/tests/lean/run/record3.lean
@@ -0,0 +1,17 @@
+import logic data.unit
+
+
+structure point (A : Type) (B : Type) :=
+mk :: (x : A) (y : B)
+
+inductive color :=
+red, green, blue
+
+structure color_point (A : Type) (B : Type) extends point A B :=
+mk :: (c : color)
+
+constant foo (p: point num num) : num
+
+constant p : color_point num num
+set_option pp.coercions true
+check foo p