From 03bbec08e5bf2a9394ab0c19713379fde3930a20 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 12 Jul 2014 09:54:22 +0100 Subject: [PATCH] perf(frontends/lean/elaborator): replace abstract with abstract_local Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 95c37c11f..378f3fe2a 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -785,7 +785,7 @@ public: } else { b = ensure_type(visit_expecting_type(b)); } - b = abstract(b, l); + b = abstract_local(b, l); return update_binding(e, d, b); } @@ -799,7 +799,7 @@ public: } else { b = visit(b); } - b = abstract(b, l); + b = abstract_local(b, l); return update_binding(e, d, b); }