From 14425bd2d356198e512e078552f2f7ed41f4b598 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 11 May 2017 14:31:37 +0200 Subject: [PATCH] fix(frontends/lean/decl_util): double-elaboration of include params --- src/frontends/lean/decl_util.cpp | 2 -- tests/lean/run/include_bug.lean | 5 +++++ 2 files changed, 5 insertions(+), 2 deletions(-) create mode 100644 tests/lean/run/include_bug.lean diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp index 6ab910e826..f3e505c4e6 100644 --- a/src/frontends/lean/decl_util.cpp +++ b/src/frontends/lean/decl_util.cpp @@ -273,8 +273,6 @@ void collect_implicit_locals(parser & p, buffer & lp_names, buffer & for (expr const & e : all_exprs) { collect_locals_ignoring_tactics(e, locals); lp_found = collect_univ_params_ignoring_tactics(e, lp_found); - if (is_local(e)) - given_params.insert(mlocal_name(e)); } collect_annonymous_inst_implicit(p, locals); sort_locals(locals.get_collected(), p, params); diff --git a/tests/lean/run/include_bug.lean b/tests/lean/run/include_bug.lean new file mode 100644 index 0000000000..c6cdaaffd5 --- /dev/null +++ b/tests/lean/run/include_bug.lean @@ -0,0 +1,5 @@ +variables x y : nat +variable xy : x = y + +include xy +lemma xyeq : x = y := xy