michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/coercion): bug add_coercion

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-25 07:43:08 -07:00
parent e9e61fec51
commit 118eae2733
1 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/library/coercion.cpp
View file

@ -247,11 +247,10 @@ static void add_coercion(coercion_ext & ext, name const & C, expr const & f, exp
list<coercion_info> infos = *it;
bool found = false;
for_each(infos, [&](coercion_info const & info) {
if (info.m_to == cls)
if (info.m_to == cls) {
ios.get_diagnostic_channel() << "replacing the coercion from '" << C << "' to '" << cls << "'";
if (is_constant(info.m_fun))
ext.m_coercions.erase(const_name(info.m_fun));
found = true;
found = true;
}
});
if (found)
infos = filter(infos, [&](coercion_info const & info) { return info.m_to != cls; });