From bf60999ede6cabfad7542563a63c09b0c2615769 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 29 Feb 2016 13:23:39 -0800 Subject: [PATCH] fix(frontends/lean/builtin_exprs): 'using' expression --- src/frontends/lean/builtin_exprs.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 446f2c203b..068fbe32ac 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -339,7 +339,7 @@ static expr parse_using_expr(parser & p, pos_info const & using_pos) { auto id_pos = p.pos(); expr l = p.parse_id(); if (!is_local(l)) - throw parser_error("invalid 'using' declaration for 'have', local expected", id_pos); + throw parser_error("invalid 'using' declaration, local expected", id_pos); expr new_l; binder_info bi = local_info(l); if (p.is_local_variable_parameter(local_pp_name(l))) { @@ -353,7 +353,7 @@ static expr parse_using_expr(parser & p, pos_info const & using_pos) { new_locals.push_back(new_l); } p.next(); // consume ',' - expr pr = parse_proof(p); + expr pr = p.parse_expr(); unsigned i = locals.size(); while (i > 0) { --i;