diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 39678fe1f3..9a86b45170 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -29,7 +29,7 @@ class type_checker; class environment; class certified_declaration; -typedef std::function extra_opaque_pred; +typedef std::function extra_opaque_pred; // NOLINT extra_opaque_pred const & no_extra_opaque(); /** diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 2b9166e34d..d94ab9a900 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -1842,8 +1842,8 @@ static int mk_type_checker(lua_State * L) { return push_type_checker_ref(L, std::make_shared(to_environment(L, 1), to_name_generator(L, 2))); } else { optional mod_idx; bool memoize; name_set extra_opaque; - extra_opaque_pred pred([=](name const & n) { return extra_opaque.contains(n); }); get_type_checker_args(L, 3, mod_idx, memoize, extra_opaque); + extra_opaque_pred pred([=](name const & n) { return extra_opaque.contains(n); }); auto t = std::make_shared(to_environment(L, 1), to_name_generator(L, 2), mk_default_converter(to_environment(L, 1), mod_idx, memoize, pred), memoize); diff --git a/tests/lua/env5.lua b/tests/lua/env5.lua index 75746d8d14..e2e9ef9223 100644 --- a/tests/lua/env5.lua +++ b/tests/lua/env5.lua @@ -56,5 +56,6 @@ assert(not pcall(function() print(tc2:check(id_1(Type, a))) end)) assert(tc2:whnf(id_2(Type, a)) == a) assert(tc2:whnf(id_2(Type, id_2(Type, a))) == a) local tc3 = type_checker(env, name_generator("foo"), {extra_opaque=name_set("id")}) +print(tc3:whnf(id_2(Type, id_2(Type, a)))) assert(tc3:whnf(id_2(Type, id_2(Type, a))) == id_2(Type, id_2(Type, a))) print(id_2(Type, id_2(Type, a)))