From 03ed74fea121ebf833e124223a28974cd84bd6de Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Tue, 4 Oct 2016 19:50:28 -0700 Subject: [PATCH] fix(inductive_compiler): generate has_sizeof for structures --- src/library/inductive_compiler/add_decl.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/inductive_compiler/add_decl.cpp b/src/library/inductive_compiler/add_decl.cpp index e23bed4023..458f1730c2 100644 --- a/src/library/inductive_compiler/add_decl.cpp +++ b/src/library/inductive_compiler/add_decl.cpp @@ -35,7 +35,7 @@ environment add_structure_declaration_aux(environment const & env, options const environment new_env = env; if (mlocal_name(ind) != get_has_sizeof_name()) - mk_has_sizeof(env, mlocal_name(ind)); + new_env = mk_has_sizeof(new_env, mlocal_name(ind)); return register_ginductive_decl(new_env, decl, ginductive_kind::BASIC); }