From 06337d04e586e17c2950c8458c0e47dadb1d38c6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 9 Jun 2018 08:11:51 -0700 Subject: [PATCH] chore(library/tactic/simplify): fix compilation error --- src/library/tactic/simplify.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp index 46aa8b8558..77b0bfde91 100644 --- a/src/library/tactic/simplify.cpp +++ b/src/library/tactic/simplify.cpp @@ -288,7 +288,7 @@ simp_result simplify_core_fn::try_user_congr(expr const & e, simp_lemma const & if (r_congr_hyp.has_proof()) simplified = true; - lean_assert(is_meta(h_rhs)); + lean_assert(is_metavar_app(h_rhs)); buffer new_val_meta_args; expr new_val_meta = get_app_args(h_rhs, new_val_meta_args); lean_assert(is_metavar(new_val_meta));