From b6be493cef0b6fa3204acc73e349aebcbd6294dd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Aug 2016 17:00:24 -0700 Subject: [PATCH] feat(frontends/lean/util): elaborate priority/precedence expressions using the new elaborator --- src/frontends/lean/notation_cmd.cpp | 2 +- src/frontends/lean/util.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index 2761fcd711..9cdf9c3a35 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -47,7 +47,7 @@ static unsigned parse_precedence_core(parser & p) { parser::local_scope scope(p, env); expr pre_val = p.parse_expr(get_max_prec()); pre_val = mk_typed_expr(mk_constant(get_num_name()), pre_val); - expr val = std::get<0>(p.old_elaborate(pre_val, list())); + expr val = p.elaborate(list(), pre_val).first; val = normalize(p.env(), val); if (optional mpz_val = to_num_core(val)) { if (!mpz_val->is_unsigned_int()) diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index e40128a3f8..6421fd9829 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -473,7 +473,7 @@ optional parse_priority(parser & p) { auto pos = p.pos(); expr pre_val = p.parse_expr(); pre_val = mk_typed_expr(mk_constant(get_num_name()), pre_val); - expr val = std::get<0>(p.old_elaborate(pre_val, list())); + expr val = p.elaborate(list(), pre_val).first; val = normalize(p.env(), val); if (optional mpz_val = to_num_core(val)) { if (!mpz_val->is_unsigned_int())