michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/tactic/goal): propagate tag (for position information) from goal to subgoal

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-02 14:47:18 -07:00
parent ee531ec0e2
commit 3e1bb96935
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/tactic/goal.cpp
View file

@ -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<expr> 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 {