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

fix: debug build

Browse source
This commit is contained in:
Leonardo de Moura 2022-04-13 13:12:53 -07:00
parent f875c2d107
commit 081dff288f
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/library/constructions/projection.cpp
View file

@ -31,7 +31,6 @@ static bool is_prop(expr type) {
}
environment mk_projections(environment const & env, name const & n, buffer<name> const & proj_names, bool inst_implicit) {
lean_assert(proj_names.size() == infer_kinds.size());
local_ctx lctx;
name_generator ngen = mk_constructions_name_generator();
constant_info ind_info = env.get(n);