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

fix(frontends/lean/elaborator): remove annotation left-over

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-12 14:14:20 -07:00
parent 563cfa73ec
commit b7dcb8f833
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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;