feat(frontends/lean/decl_cmds): use new elaborator for variable, parameter and constant commands

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<expr> 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);

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

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