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

fix(library/tactic/clear_tactic): fail if hypothesis has dependecies

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-09 17:19:49 -07:00
parent d5a648a12a
commit 69cc58dbda
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/tactic/clear_tactic.cpp
View file

@ -20,6 +20,8 @@ expr clear(metavar_context & mctx, expr const & mvar, expr const & H) {
throw exception(sstream() << "clear tactic failed, unknown '" << local_pp_name(H) << "' hypothesis");
if (depends_on(g->get_type(), 1, &H))
throw exception(sstream() << "clear tactic failed, target type depends on '" << local_pp_name(H) << "'");
if (optional<local_decl> d2 = lctx.has_dependencies(*d))
throw exception(sstream() << "clear tactic failed, hypothesis '" << d2->get_pp_name() << "' depends on '" << local_pp_name(H) << "'");
lctx.clear(*d);
expr new_mvar = mctx.mk_metavar_decl(lctx, g->get_type());
mctx.assign(mvar, new_mvar);