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

Add small optimization.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-10 21:02:45 -07:00
parent 7ebaac62a8
commit 3a1514982f
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/kernel/type_check.cpp
View file

@ -128,7 +128,10 @@ struct infer_type_fn {
buffer << "\nin context:\n" << ctx;
throw exception(buffer.str());
}
f_t = instantiate(abst_body(f_t), c);
if (closed(c))
f_t = instantiate_with_closed(abst_body(f_t), c);
else
f_t = instantiate(abst_body(f_t), c);
i++;
if (i == num) {
r = f_t;