diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 4a01edf86..26c69838c 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1302,7 +1302,7 @@ expr parser::parse_notation_core(parse_table t, expr * left, bool as_tactic) { r = instantiate_rev(r, new_args.size(), new_args.data()); cs.push_back(r); } else { - lean_assert(nargs.empty() && ps_sz.empty()); + lean_assert(nargs.empty() && scoped_info.empty()); if (args.empty()) { // Notation does not have arguments. Thus, the info-manager should treat is as a single thing. r = mk_notation_info(r, r.get_tag()); diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index 694d4c3ad..a19147666 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -198,8 +198,8 @@ environment certified_inductive_decl::add_constant(environment const & env, name } environment certified_inductive_decl::add_core(environment const & env, bool update_ext_only) const { - lean_assert(m_data); - lean_assert(length(m_data) == length(m_elim_types)); + lean_assert(m_decl_data); + lean_assert(length(m_decl_data) == length(m_elim_types)); environment new_env = env; inductive_env_ext ext(get_extension(new_env)); level_param_names levels = m_levels;