From 9b61b18eaac41b6f2bc5e5eb00dc0021f1202af1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 23 Sep 2014 15:26:05 -0700 Subject: [PATCH] perf(kernel/replace_visitor): use more expensive/precise cache It does not use pointer equality, but structural equality --- src/kernel/replace_visitor.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/kernel/replace_visitor.h b/src/kernel/replace_visitor.h index a0dd57608c..bfe389e2ea 100644 --- a/src/kernel/replace_visitor.h +++ b/src/kernel/replace_visitor.h @@ -16,7 +16,7 @@ namespace lean { */ class replace_visitor { protected: - typedef expr_map cache; + typedef expr_bi_struct_map cache; cache m_cache; expr save_result(expr const & e, expr && r, bool shared); virtual expr visit_sort(expr const &);