max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/tactic/match_tactic): check whether all meta-variables have been assigned

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-27 14:53:42 +01:00
parent d487a59c23
commit 23565ff43c
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/tactic/match_tactic.cpp
View file

@ -144,6 +144,14 @@ vm_obj tactic_match_pattern_core(vm_obj const & m, vm_obj const & p, vm_obj cons
type_context ctx = mk_type_context_for(s, m);
type_context::tmp_mode_scope scope(ctx, nuvars, nmvars);
if (ctx.is_def_eq(t, to_expr(e))) {
for (unsigned i = 0; i < nuvars; i++) {
if (!ctx.get_tmp_uvar_assignment(i))
return mk_tactic_exception(sstream() << "match_pattern failed, universe meta-variable #" << i << " has not been assigned.", to_tactic_state(s));
}
for (unsigned i = 0; i < nmvars; i++) {
if (!ctx.get_tmp_mvar_assignment(i))
return mk_tactic_exception(sstream() << "match_pattern failed, meta-variable #" << i << " has not been assigned.", to_tactic_state(s));
}
buffer<expr> inst_os;
for (expr const & o : os) {
inst_os.push_back(ctx.instantiate_mvars(o));