From c27167f445b2b584d2b975a96fbd5944bae5250a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 11 Feb 2019 15:35:03 -0800 Subject: [PATCH] fix(library/compiler/ll_infer_type): use extern_attribute --- src/library/compiler/compiler.cpp | 2 +- src/library/compiler/ll_infer_type.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp index 9c2befdee3..6ddefebbe5 100644 --- a/src/library/compiler/compiler.cpp +++ b/src/library/compiler/compiler.cpp @@ -134,7 +134,7 @@ environment compile(environment const & env, options const & opts, names const & } if (length(cs) == 1 && is_extern_constant(env, head(cs))) { - /* Generate boxed version for native constant if needed. */ + /* Generate boxed version for extern/native constant if needed. */ unsigned arity = *get_extern_constant_arity(env, head(cs)); if (optional> p = mk_boxed_version(env, head(cs), arity)) { /* Remark: we don't need boxed version for the bytecode. */ diff --git a/src/library/compiler/ll_infer_type.cpp b/src/library/compiler/ll_infer_type.cpp index b04367a3d5..d3d9347af0 100644 --- a/src/library/compiler/ll_infer_type.cpp +++ b/src/library/compiler/ll_infer_type.cpp @@ -7,7 +7,7 @@ Author: Leonardo de Moura #include "runtime/flet.h" #include "kernel/instantiate.h" #include "library/compiler/util.h" -#include "library/compiler/builtin.h" +#include "library/compiler/extern_attribute.h" namespace lean { /* Infer type of expressions in ENF or LLNF. */ @@ -147,7 +147,7 @@ class ll_infer_type_fn { } expr infer_constant(expr const & e) { - if (optional type = get_native_constant_ll_type(env(), const_name(e))) { + if (optional type = get_extern_constant_ll_type(env(), const_name(e))) { return *type; } else if (is_constructor(env(), const_name(e))) { return infer_constructor_type(e);