From 709b5ce90fdaa0ba46f18971a96d2f64d659cfe2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Jul 2014 21:16:49 -0700 Subject: [PATCH] fix(kernel/justification): duplicate position Signed-off-by: Leonardo de Moura --- src/kernel/justification.cpp | 7 +++++-- tests/lean/empty.lean.expected.out | 2 +- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/kernel/justification.cpp b/src/kernel/justification.cpp index 0f640b6688..5d652eb2f6 100644 --- a/src/kernel/justification.cpp +++ b/src/kernel/justification.cpp @@ -317,8 +317,11 @@ justification mk_justification(optional const & s, pp_jst_fn const & fn) { return justification(new (get_asserted_allocator().allocate()) asserted_cell(fn, s)); } justification mk_justification(optional const & s, pp_jst_sfn const & fn) { - return mk_justification(s, [=](formatter const & fmt, pos_info_provider const * p, substitution const & subst) { - return compose(to_pos(s, p), fn(fmt, subst)); }); + return mk_justification(s, [=](formatter const & fmt, pos_info_provider const *, substitution const & subst) { + // Remark: we are not using to_pos(s, p) anymore because we don't try to display complicated error messages anymore. + // return compose(to_pos(s, p), fn(fmt, subst)); + return fn(fmt, subst); + }); } justification mk_justification(char const * msg, optional const & s) { std::string _msg(msg); diff --git a/tests/lean/empty.lean.expected.out b/tests/lean/empty.lean.expected.out index 9cc3bc9188..41aed30d71 100644 --- a/tests/lean/empty.lean.expected.out +++ b/tests/lean/empty.lean.expected.out @@ -1,2 +1,2 @@ -empty.lean:5:25: error: empty.lean:5:25: failed to synthesize placeholder +empty.lean:5:25: error: failed to synthesize placeholder ⊢ inhabited Empty