From 57c85221fec9156aef53097e4d3349c153376347 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 8 Oct 2014 13:36:00 -0700 Subject: [PATCH] fix(frontends/lean): collect used universe levels after elaboration in the check command --- src/frontends/lean/builtin_cmds.cpp | 4 ++-- tests/lean/run/mor.lean | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index a23dfe57c..49e35cfb6 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -131,10 +131,10 @@ environment end_scoped_cmd(parser & p) { static std::tuple parse_local_expr(parser & p) { expr e = p.parse_expr(); list ctx = p.locals_to_context(); - level_param_names ls = to_level_param_names(collect_univ_params(e)); level_param_names new_ls; std::tie(e, new_ls) = p.elaborate_relaxed(e, ctx); - return std::make_tuple(e, append(ls, new_ls)); + level_param_names ls = to_level_param_names(collect_univ_params(e)); + return std::make_tuple(e, ls); } environment check_cmd(parser & p) { diff --git a/tests/lean/run/mor.lean b/tests/lean/run/mor.lean index 06e0646a0..126a492ad 100644 --- a/tests/lean/run/mor.lean +++ b/tests/lean/run/mor.lean @@ -11,5 +11,6 @@ namespace morphism parameter {ob : Type} parameter {C : category ob} variables {a b c d : ob} {h : mor c d} {g : mor b c} {f : mor a b} + check mor a b end end morphism