From 19bf71eb9ced26d85e0873af4e2e7e974d31157b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 9 Nov 2018 13:18:28 -0800 Subject: [PATCH] chore(library/compiler/simp_app_args): use `ll_infer_type` --- src/library/compiler/simp_app_args.cpp | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/src/library/compiler/simp_app_args.cpp b/src/library/compiler/simp_app_args.cpp index 25508a478b..4a7d4a1f5b 100644 --- a/src/library/compiler/simp_app_args.cpp +++ b/src/library/compiler/simp_app_args.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "kernel/instantiate.h" #include "library/compiler/util.h" +#include "library/compiler/ll_infer_type.h" namespace lean { /* Make sure every argument of applications and projections is a free variable (or neutral element). */ @@ -75,11 +76,7 @@ class simp_app_args_fn { m_fvars.push_back(fvar); return fvar; } else if (is_constant(e)) { - expr type; - if (optional info = env().find(const_name(e))) - type = mk_runtime_type(m_st, m_lctx, info->get_type()); - else - type = mk_enf_object_type(); // TODO(Leo): improve + expr type = ll_infer_type(env(), e); expr fvar = m_lctx.mk_local_decl(ngen(), next_name(), type, e); m_fvars.push_back(fvar); return fvar;