max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/compiler/ll_infer_type): use extern_attribute

Browse source
This commit is contained in:
Leonardo de Moura 2019-02-11 15:35:03 -08:00
parent 9c3675f58f
commit c27167f445
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/compiler/compiler.cpp
View file

@ -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<pair<environment, comp_decl>> p = mk_boxed_version(env, head(cs), arity)) {
/* Remark: we don't need boxed version for the bytecode. */

4
src/library/compiler/ll_infer_type.cpp
View file

@ -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<expr> type = get_native_constant_ll_type(env(), const_name(e))) {
if (optional<expr> 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);