From 9a9e975bc85076b54cfde19d55be9ee936fe82ea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 30 Jun 2015 14:00:41 -0700 Subject: [PATCH] feat(frontends/lean/migrate_cmd): ignore derived transitive instances in the migrate command --- src/frontends/lean/migrate_cmd.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/frontends/lean/migrate_cmd.cpp b/src/frontends/lean/migrate_cmd.cpp index c76945ae1d..5f76271657 100644 --- a/src/frontends/lean/migrate_cmd.cpp +++ b/src/frontends/lean/migrate_cmd.cpp @@ -172,6 +172,11 @@ struct migrate_cmd_fn { out() << "skipped '" << d.get_name() << "': coercions are ignored\n"; return; // we don't migrate coercions } + if (is_derived_trans_instance(m_env, d_name)) { + if (m_trace) + out() << "skipped '" << d.get_name() << "': derived transitive instances are ignored\n"; + return; // we don't migrate coercions + } bool renamed = false; name short_name, full_name;