From 0a6f571f07fae4b01f490850eb840c488eb2ffac Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 19 Sep 2016 11:29:03 -0700 Subject: [PATCH] fix(library/tactic/simplifier/simplifier): assertion --- src/library/tactic/simplifier/simplifier.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/library/tactic/simplifier/simplifier.cpp b/src/library/tactic/simplifier/simplifier.cpp index 0aec2c74d2..ef821805ee 100644 --- a/src/library/tactic/simplifier/simplifier.cpp +++ b/src/library/tactic/simplifier/simplifier.cpp @@ -1084,7 +1084,13 @@ simp_result simplifier::try_congr(expr const & e, user_congr_lemma const & cl) { flet set_ctx_slss(m_ctx_slss, m_contextual ? add_to_slss(m_ctx_slss, local_factory.as_buffer()) : m_ctx_slss); h_lhs = tmp_tctx.instantiate_mvars(h_lhs); - lean_assert(!has_metavar(h_lhs)); + /* TODO(Leo, Daniel): the original assertion was !has_metavar(h_lhs). + It is incorrect. I got an assertion violation when processing + a term containing universe meta-variables. So, I relaxed it to !has_expr_metavar(h_lhs). + We should investigate this. Example: what happens if the input expression has + regular meta-variables? Perhaps, the right assertion is: h_lhs does *not* have temporary + universe and regular meta-variables. */ + lean_assert(!has_expr_metavar(h_lhs)); if (m_contextual) { freset reset_cache(m_cache);