diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index b114ac280..5d617cfd6 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -295,7 +295,7 @@ public: auto choice_fn = [=](expr const & /* t */, substitution const & s, name_generator const & /* ngen */) { return choose(std::make_shared(*this, e, ctx, s)); }; - justification j = mk_justification("overloading", some_expr(e)); + justification j = mk_justification("none of the overloads is applicable", some_expr(e)); add_cnstr(mk_choice_cnstr(m, choice_fn, false, j)); return m; }