From e9338669dcd41f8a67ab93b63ce271c8117c342f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Jan 2015 13:30:12 -0800 Subject: [PATCH] feat(library/definitional/equations): show implicit arguments (by default) in equations compiler error messages --- src/library/definitional/equations.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/library/definitional/equations.cpp b/src/library/definitional/equations.cpp index f741d8a99..1616a97f0 100644 --- a/src/library/definitional/equations.cpp +++ b/src/library/definitional/equations.cpp @@ -560,10 +560,12 @@ class equation_compiler_fn { // every variable in the local_ctx must be "reachable". if (!reachable_vars.contains(mlocal_name(v))) { throw_error(lhs, [=](formatter const & fmt) { + options o = fmt.get_options().update_if_undef(get_pp_implicit_name(), true); + formatter new_fmt = fmt.update_options(o); format r("invalid equation left-hand-side, variable '"); r += format(local_pp_name(v)); r += format("' only occurs in inaccessible terms in the following equation left-hand-side"); - r += pp_indent_expr(fmt, lhs); + r += pp_indent_expr(new_fmt, lhs); return r; }); }