From 23565ff43ca6aa94f270666a48eb42de0f2487f4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 Jun 2016 14:53:42 +0100 Subject: [PATCH] fix(library/tactic/match_tactic): check whether all meta-variables have been assigned --- src/library/tactic/match_tactic.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/library/tactic/match_tactic.cpp b/src/library/tactic/match_tactic.cpp index c253625bfa..9c7793a5e0 100644 --- a/src/library/tactic/match_tactic.cpp +++ b/src/library/tactic/match_tactic.cpp @@ -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 inst_os; for (expr const & o : os) { inst_os.push_back(ctx.instantiate_mvars(o));