From 69cc58dbdacf2322f89368259fb3f0f1ab756ef3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 9 Jul 2016 17:19:49 -0700 Subject: [PATCH] fix(library/tactic/clear_tactic): fail if hypothesis has dependecies --- src/library/tactic/clear_tactic.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/library/tactic/clear_tactic.cpp b/src/library/tactic/clear_tactic.cpp index a4b30483b0..06ae790004 100644 --- a/src/library/tactic/clear_tactic.cpp +++ b/src/library/tactic/clear_tactic.cpp @@ -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 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);