From 3e1bb9693594532d3a895e8afd13da3ba644ddfd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 Jul 2014 14:47:18 -0700 Subject: [PATCH] feat(library/tactic/goal): propagate tag (for position information) from goal to subgoal Signed-off-by: Leonardo de Moura --- src/library/tactic/goal.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp index 01312a8f3b..63520464b1 100644 --- a/src/library/tactic/goal.cpp +++ b/src/library/tactic/goal.cpp @@ -81,14 +81,14 @@ expr goal::abstract(expr const & v) const { expr goal::mk_meta(name const & n, expr const & type, bool only_contextual) const { buffer locals; - get_app_args(m_meta, locals); + expr this_mvar = get_app_args(m_meta, locals); if (only_contextual) { auto new_end = std::remove_if(locals.begin(), locals.end(), [](expr const & l) { return !local_info(l).is_contextual(); }); locals.shrink(locals.size() - (locals.end() - new_end)); } - expr mvar = mk_metavar(n, Pi(locals, type)); - return mk_app(mvar, locals); + expr mvar = copy_tag(this_mvar, mk_metavar(n, Pi(locals, type))); + return copy_tag(m_meta, mk_app(mvar, locals)); } goal goal::instantiate_metavars(substitution const & s) const {