From b6dd1269b9d5a871083687a984678700610088c8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Feb 2015 10:38:45 -0800 Subject: [PATCH] feat(frontends/lean/builtin_exprs): make 'obtain' arguments visible by default --- src/frontends/lean/builtin_exprs.cpp | 9 --------- 1 file changed, 9 deletions(-) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 71b03e327..77bda48a7 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -343,15 +343,6 @@ static expr parse_obtain(parser & p, unsigned, expr const *, pos_info const & po unsigned num_ps = ps.size(); if (num_ps < 2) throw parser_error("invalid 'obtain' expression, at least 2 binders expected", b_pos); - bool is_visible = false; - if (p.curr_is_token(get_visible_tk())) { - p.next(); - is_visible = true; - } - if (!is_visible) { - expr H = ps[num_ps-1]; - ps[num_ps-1] = update_local(H, mlocal_type(H), local_info(H).update_contextual(false)); - } p.check_token_next(get_comma_tk(), "invalid 'obtain' expression, ',' expected"); p.check_token_next(get_from_tk(), "invalid 'obtain' expression, 'from' expected"); expr H1 = p.parse_expr();