From b7dcb8f833971e5cd1c83886cb35c6427bf96bac Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 12 Sep 2014 14:14:20 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): remove annotation left-over --- src/frontends/lean/elaborator.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 3cfbf8d6c3..14203591ab 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -708,6 +708,8 @@ public: return visit(get_annotation_arg(e), cs); } else if (is_typed_expr(e)) { return visit_typed_expr(e, cs); + } else if (is_implicit(e)) { + return visit_core(get_implicit_arg(e), cs); } else { switch (e.kind()) { case expr_kind::Local: return e;