max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/lean/vm_elaborator): correctly set up declaration_info_scope

Browse source
This commit is contained in:
Sebastian Ullrich 2019-02-15 19:16:50 +01:00 • committed by Leonardo de Moura
parent d083f8457a
commit f6fde1a53d
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/vm_elaborator.cpp
View file

@ -289,7 +289,7 @@ void elab_defs_cmd(parser & p, expr const & cmd) {
get_app_args(mdata_expr(cmd), args);
auto meta = to_cmd_meta(p.env(), args[0]);
auto kind = static_cast<decl_cmd_kind>(lit_value(args[1]).get_nat().get_small_value());
declaration_info_scope scope(p, kind, meta.m_modifiers);
declaration_info_scope scope(p, kind, meta);
buffer<name> lp_names;
buffer<expr> fns, params;
/* TODO(Leo): allow a different doc string for each function in a mutual definition. */