From 35ddd49e7ac2e676a858e43c46ab192fc08a453c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Mar 2019 13:53:02 -0700 Subject: [PATCH] chore(frontends/lean/structure_cmd): `toParent` instead of `to_Parent` --- src/frontends/lean/structure_cmd.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 3189832095..4c7ec94369 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -492,7 +492,7 @@ struct structure_cmd_fn { if (auto const & ref = m_parent_refs[i]) fname = *ref; else - fname = name(parent_name.get_string()).append_before("to_"); + fname = name(parent_name.get_string()).append_before("to"); binder_info bi = mk_binder_info(); if (m_meta_info.m_attrs.has_class() && is_class(m_env, parent_name)) // make superclass fields inst implicit @@ -1196,7 +1196,7 @@ struct structure_cmd_fn { non_unique.insert(n, idx+1); n = n.append_after(idx); } - name coercion_name = m_name + n.append_before("to_"); + name coercion_name = m_name + n.append_before("to"); coercion_names.push_back(coercion_name); } }