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

perf(frontends/lean/elaborator): replace abstract with abstract_local

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-12 09:54:22 +01:00
parent 319b1fb8d1
commit 03bbec08e5
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/elaborator.cpp
View file

@ -785,7 +785,7 @@ public:
} else { } else {
b = ensure_type(visit_expecting_type(b)); b = ensure_type(visit_expecting_type(b));
} }
b = abstract(b, l); b = abstract_local(b, l);
return update_binding(e, d, b); return update_binding(e, d, b);
} }
@ -799,7 +799,7 @@ public:
} else { } else {
b = visit(b); b = visit(b);
} }
b = abstract(b, l); b = abstract_local(b, l);
return update_binding(e, d, b); return update_binding(e, d, b);
} }