From e2a7d78dd627759c94de063374100468e627d107 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 May 2018 17:57:33 -0700 Subject: [PATCH] chore(util/name): remove dead code --- src/util/name.h | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/util/name.h b/src/util/name.h index 86a0a66ff7..9364420467 100644 --- a/src/util/name.h +++ b/src/util/name.h @@ -198,8 +198,6 @@ public: } } void serialize(serializer & s) const { s.write_object(raw()); } - struct ptr_hash { unsigned operator()(name const & n) const { return std::hash()(n.raw()); } }; - struct ptr_eq { bool operator()(name const & n1, name const & n2) const { return n1.raw() == n2.raw(); } }; }; name string_to_name(std::string const & str);