From f4e1e92807d71b6777fee821eb5fdb9c69eef435 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Aug 2016 17:10:45 -0700 Subject: [PATCH] feat(frontends/lean/decl_cmds): use new elaborator for variable, parameter and constant commands --- src/frontends/lean/decl_cmds.cpp | 2 +- tests/lean/858.lean.expected.out | 5 +++-- tests/lean/const.lean | 2 +- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index ee17c630f8..9c59372351 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -300,7 +300,7 @@ static environment variable_cmd_core(parser & p, variable_kind k, bool is_protec } level_param_names new_ls; list ctx = p.locals_to_context(); - std::tie(type, new_ls) = p.old_elaborate_type(type, ctx); + std::tie(type, new_ls) = p.elaborate_type(ctx, type); if (k == variable_kind::Variable || k == variable_kind::Parameter) update_local_levels(p, new_ls, k == variable_kind::Variable); return declare_var(p, p.env(), n, append(ls, new_ls), type, k, bi, pos, is_protected); diff --git a/tests/lean/858.lean.expected.out b/tests/lean/858.lean.expected.out index 574ab706ab..784c6ef931 100644 --- a/tests/lean/858.lean.expected.out +++ b/tests/lean/858.lean.expected.out @@ -1,2 +1,3 @@ -858.lean:2:2: error: failed to add declaration 'n' to local context, type has metavariables - ?M_1 → ℕ +858.lean:2:18: error: don't know how to synthesize placeholder +state: +⊢ Type diff --git a/tests/lean/const.lean b/tests/lean/const.lean index 6548a3dbc8..2e4bba4254 100644 --- a/tests/lean/const.lean +++ b/tests/lean/const.lean @@ -11,7 +11,7 @@ set_option pp.implicit true section variable A : Type variable S : inhabited A - variable B : @bla A _ + variable B : @bla A S check B check @foo A S end