From 3e6b80d38c70e382f66b857b7bc68f4614a646ba Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 23 Jul 2015 18:43:56 -0700 Subject: [PATCH] feat(library/util): disable local constant purification when pretty printing goals This feature generates confusion. --- src/library/util.cpp | 6 ++++-- tests/lean/assert_fail.lean.expected.out | 2 +- tests/lean/assert_tac2.lean.expected.out | 4 ++-- 3 files changed, 7 insertions(+), 5 deletions(-) diff --git a/src/library/util.cpp b/src/library/util.cpp index e267993fa..164812520 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -822,9 +822,11 @@ justification mk_type_mismatch_jst(expr const & v, expr const & v_type, expr con }); } -format format_goal(formatter const & fmt, buffer const & hyps, expr const & conclusion, substitution const & s) { +format format_goal(formatter const & _fmt, buffer const & hyps, expr const & conclusion, substitution const & s) { substitution tmp_subst(s); - options const & opts = fmt.get_options(); + options opts = _fmt.get_options(); + opts = opts.update_if_undef(get_pp_purify_locals_name(), false); + formatter fmt = _fmt.update_options(opts); unsigned indent = get_pp_indent(opts); bool unicode = get_pp_unicode(opts); bool compact = get_pp_compact_goals(opts); diff --git a/tests/lean/assert_fail.lean.expected.out b/tests/lean/assert_fail.lean.expected.out index 07deb34a6..a92e471ca 100644 --- a/tests/lean/assert_fail.lean.expected.out +++ b/tests/lean/assert_fail.lean.expected.out @@ -4,7 +4,7 @@ H : b ∧ a ⊢ a a b : Prop, -H_1 : b ∧ a, +H : b ∧ a, H : a ⊢ a ∧ b assert_fail.lean:4:0: error: failed to add declaration 'example' to environment, value has metavariables diff --git a/tests/lean/assert_tac2.lean.expected.out b/tests/lean/assert_tac2.lean.expected.out index c821e07dd..9cf6e7403 100644 --- a/tests/lean/assert_tac2.lean.expected.out +++ b/tests/lean/assert_tac2.lean.expected.out @@ -2,7 +2,7 @@ assert_tac2.lean:11:2: proof state a b c : ℕ, h1 : a = 2, h2 : b = 3, -H_2 : a + b = 2 + b, -H_1 : a + b = 2 + 3, +H : a + b = 2 + b, +H : a + b = 2 + 3, H : a + b = 5 ⊢ 5 + c = c + 5