From ee46befd26a5e8e2bd90d5729375cb3aa9026bfc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 2 Aug 2016 13:16:43 -0700 Subject: [PATCH] chore(frontends/lean/elaborator): cleanup --- src/frontends/lean/elaborator.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 7f905b421e..ca8158cdcd 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -679,7 +679,7 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer< list main_idxs = info.m_explicit_idxs; buffer> postponed_args; // mark arguments that must be elaborated in the second pass. { - checkpoint C(*this); + checkpoint C1(*this); while (is_pi(type)) { expr const & d = binding_domain(type); binder_info const & bi = binding_info(type); @@ -687,9 +687,9 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer< optional postponed; if (std::find(main_idxs.begin(), main_idxs.end(), i) != main_idxs.end()) { { - checkpoint C(*this); + checkpoint C2(*this); new_arg = visit(args[j], some_expr(d)); - process_checkpoint(C); + process_checkpoint(C2); new_arg = instantiate_mvars(new_arg); } j++; @@ -729,7 +729,7 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer< for (; j < args.size(); j++) { new_args.push_back(visit(args[j], none_expr())); } - process_checkpoint(C); + process_checkpoint(C1); } /* Compute expected_type for the recursor application without extra arguments */