From 04670c4127becd80abf51be78fb6ef17fe123c62 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 3 May 2019 20:03:03 -0700 Subject: [PATCH] fix(library/compiler/struct_cases_on): bug and missing case --- src/library/compiler/struct_cases_on.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/library/compiler/struct_cases_on.cpp b/src/library/compiler/struct_cases_on.cpp index 790faf7a9c..b917202a39 100644 --- a/src/library/compiler/struct_cases_on.cpp +++ b/src/library/compiler/struct_cases_on.cpp @@ -154,7 +154,7 @@ class struct_cases_on_fn { while (is_let(e)) { lean_assert(!has_loose_bvars(let_type(e))); expr type = let_type(e); - expr val = instantiate_rev(let_value(e), fvars.size(), fvars.data()); + expr val = visit(instantiate_rev(let_value(e), fvars.size(), fvars.data())); name n = let_name(e); e = let_body(e); expr new_fvar = m_lctx.mk_local_decl(ngen(), n, type, val); @@ -177,7 +177,7 @@ class struct_cases_on_fn { e = mk_let(decl.get_user_name(), type, aval, e); if (should_add_cases_on(decl)) { lean_assert(is_proj(val)); - expr major = proj_expr(val); + expr major = proj_expr(aval); buffer field_types; get_struct_field_types(m_st, proj_sname(val), field_types); e = lift_loose_bvars(e, field_types.size());