From f6fde1a53dc6aae3a8824b53461df32c856cec3f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 15 Feb 2019 19:16:50 +0100 Subject: [PATCH] fix(frontends/lean/vm_elaborator): correctly set up `declaration_info_scope` --- src/frontends/lean/vm_elaborator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/vm_elaborator.cpp b/src/frontends/lean/vm_elaborator.cpp index fde1837e9a..25ee68bf95 100644 --- a/src/frontends/lean/vm_elaborator.cpp +++ b/src/frontends/lean/vm_elaborator.cpp @@ -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(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 lp_names; buffer fns, params; /* TODO(Leo): allow a different doc string for each function in a mutual definition. */