From 6d2df80a17f3bb6355cfd590e9d60dec8d920411 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 7 Sep 2014 09:36:03 -0700 Subject: [PATCH] feat(frontends/lean/server): use '?a' instead of '?M_i' for implicit arguments when displaying FINDP and FINDG matches Signed-off-by: Leonardo de Moura --- src/frontends/lean/server.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index 1214b92f8c..3d8d8b2dde 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -498,13 +498,14 @@ void server::display_decl(name const & short_name, name const & long_name, envir io_state_stream out = regular(env, m_ios).update_options(o); expr type = d.get_type(); if (LEAN_FIND_CONSUME_IMPLICIT) { - name_generator ngen("M"); while (true) { if (!is_pi(type)) break; if (!binding_info(type).is_implicit()) break; - expr m = mk_metavar(ngen.next(), binding_domain(type)); + std::string q("?"); + q += binding_name(type).to_string(); + expr m = mk_constant(name(q.c_str())); type = instantiate(binding_body(type), m); } }