From 38c433dbecd9dcf24971e7351fea08200ee33958 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Oct 2015 15:38:45 -0700 Subject: [PATCH] fix(frontends/lean/util): bug when parsing priorities --- src/frontends/lean/util.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 17b51d0ec..5c2a750a8 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -477,7 +477,7 @@ optional parse_priority(parser & p) { if (p.curr_is_token(get_priority_tk())) { p.next(); auto pos = p.pos(); - expr pre_val = p.parse_expr(get_max_prec()); + expr pre_val = p.parse_expr(); pre_val = mk_typed_expr(mk_constant(get_num_name()), pre_val); expr val = std::get<0>(p.elaborate(pre_val, list())); val = normalize(p.env(), val);