michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

perf(library/unifier): avoid unnecessary wasteful computation

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-16 17:16:49 -07:00
parent fe484b26f3
commit 8974b52f7b
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/unifier.cpp
View file

@ -1440,7 +1440,7 @@ struct unifier_fn {
num++;
t = binding_body(t);
}
if (num == margs.size())
if (num >= margs.size())
return mtype;
return ensure_sufficient_args_core(mtype, 0, cs);
}