From 16a6a54df1432431da6e9d91aa73319f99a80de2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 22 Sep 2013 16:41:51 -0700 Subject: [PATCH] Fix abuse of operator-> overload Signed-off-by: Leonardo de Moura --- src/kernel/metavar.cpp | 16 ++++++++-------- src/util/pvector.h | 1 - 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 5d7dada1a..7b575d016 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -61,18 +61,18 @@ expr metavar_env::get_subst(unsigned midx) const { } expr metavar_env::get_type(unsigned midx, unification_problems & up) { - auto p = m_env[midx]; - expr t = p->m_type; + data const & d = m_env[midx]; + expr t = d.m_type; if (t) { return t; } else { t = mk_metavar(); - expr s = p->m_subst; - m_env[midx] = data(s, t, p->m_ctx); + expr s = d.m_subst; + m_env[midx] = data(s, t, d.m_ctx); if (s) - up.add_type_of_eq(p->m_ctx, s, t); + up.add_type_of_eq(d.m_ctx, s, t); else - up.add_type_of_eq(p->m_ctx, ::lean::mk_metavar(midx), t); + up.add_type_of_eq(d.m_ctx, ::lean::mk_metavar(midx), t); return t; } } @@ -84,8 +84,8 @@ expr metavar_env::get_type(unsigned midx) const { void metavar_env::assign(unsigned midx, expr const & v) { inc_timestamp(); lean_assert(!is_assigned(midx)); - auto p = m_env[midx]; - m_env[midx] = data(v, p->m_type, p->m_ctx); + data const & d = m_env[midx]; + m_env[midx] = data(v, d.m_type, d.m_ctx); } context const & metavar_env::get_context(unsigned midx) const { diff --git a/src/util/pvector.h b/src/util/pvector.h index c6f229212..4bc8b1539 100644 --- a/src/util/pvector.h +++ b/src/util/pvector.h @@ -351,7 +351,6 @@ public: ref(pvector & v, unsigned i):m_vector(v), m_idx(i) {} ref & operator=(T const & a) { m_vector.set(m_idx, a); return *this; } operator T const &() const { return m_vector.get(m_idx); } - T const * operator->() const { return &(m_vector.get(m_idx)); } }; T const & operator[](unsigned i) const { return get(i); }