From 3d2ff8a76d42bcabd81ede5e4310b70d655fdce2 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Tue, 4 Oct 2016 20:14:22 -0700 Subject: [PATCH] chore(frontends/lean/inductive_cmd): readable name for ind result level placeholder --- src/frontends/lean/inductive_cmds.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp index fea6cfbe16..0831eaa299 100644 --- a/src/frontends/lean/inductive_cmds.cpp +++ b/src/frontends/lean/inductive_cmds.cpp @@ -38,9 +38,9 @@ Authors: Daniel Selsam, Leonardo de Moura #include "frontends/lean/inductive_cmds.h" namespace lean { -static name * g_tmp_prefix = nullptr; +static name * g_tmp_global_univ_name = nullptr; -static name tmp_global_univ_name() { return name(*g_tmp_prefix, "u"); } +static name tmp_global_univ_name() { return *g_tmp_global_univ_name; } static void convert_params_to_kernel(elaborator & elab, buffer const & lctx_params, buffer & kernel_params) { for (unsigned i = 0; i < lctx_params.size(); ++i) { @@ -550,10 +550,10 @@ void initialize_inductive_cmds() { register_trace_class(name({"inductive", "finalize"})); register_trace_class(name({"inductive", "lp_names"})); - g_tmp_prefix = new name(name::mk_internal_unique_name()); + g_tmp_global_univ_name = new name(mk_tagged_fresh_name("_inductive_result_level")); } void finalize_inductive_cmds() { - delete g_tmp_prefix; + delete g_tmp_global_univ_name; } }